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

Theorem ancli 321
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 304 1 (𝜑 → (𝜑𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107
This theorem is referenced by:  pm4.45im  332  mo23  2060  barbari  2121  cesaro  2127  camestros  2128  calemos  2138  swopo  4291  elrnrexdm  5635  tfrcl  6343  ixpsnf1o  6714  fidcenumlemrk  6931  subhalfnqq  7376  enq0ref  7395  prarloc  7465  letrp1  8764  p1le  8765  peano2uz2  9319  uzind  9323  uzid  9501  qreccl  9601  fprodsplit1f  11597
  Copyright terms: Public domain W3C validator