ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ancli GIF version

Theorem ancli 306
Description: Deduction conjoining antecedent to left of consequent. (Contributed by NM, 12-Aug-1993.)
Hypothesis
Ref Expression
ancli.1 (𝜑𝜓)
Assertion
Ref Expression
ancli (𝜑 → (𝜑𝜓))

Proof of Theorem ancli
StepHypRef Expression
1 id 19 . 2 (𝜑𝜑)
2 ancli.1 . 2 (𝜑𝜓)
31, 2jca 290 1 (𝜑 → (𝜑𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101
This theorem is referenced by:  pm4.45im  317  mo23  1941  barbari  2002  cesaro  2008  camestros  2009  calemos  2019  swopo  4043  elrnrexdm  5306  subhalfnqq  6512  enq0ref  6531  prarloc  6601  letrp1  7814  p1le  7815  peano2uz2  8345  uzind  8349  uzid  8487  qreccl  8576
  Copyright terms: Public domain W3C validator