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

Theorem ancli 310
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 294 1 (𝜑 → (𝜑𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 105
This theorem is referenced by:  pm4.45im  321  mo23  1957  barbari  2018  cesaro  2024  camestros  2025  calemos  2035  swopo  4071  elrnrexdm  5334  subhalfnqq  6570  enq0ref  6589  prarloc  6659  letrp1  7889  p1le  7890  peano2uz2  8404  uzind  8408  uzid  8583  qreccl  8674
  Copyright terms: Public domain W3C validator