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  2047  barbari  2108  cesaro  2114  camestros  2115  calemos  2125  swopo  4266  elrnrexdm  5606  tfrcl  6311  ixpsnf1o  6681  fidcenumlemrk  6898  subhalfnqq  7334  enq0ref  7353  prarloc  7423  letrp1  8719  p1le  8720  peano2uz2  9271  uzind  9275  uzid  9453  qreccl  9551  fprodsplit1f  11531
  Copyright terms: Public domain W3C validator