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

Theorem ancli 321
Description: Deduction conjoining antecedent to left of consequent. (Contributed by NM, 12-Aug-1993.)
Hypothesis
Ref Expression
ancli.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
ancli  |-  ( ph  ->  ( ph  /\  ps ) )

Proof of Theorem ancli
StepHypRef Expression
1 id 19 . 2  |-  ( ph  ->  ph )
2 ancli.1 . 2  |-  ( ph  ->  ps )
31, 2jca 304 1  |-  ( ph  ->  ( ph  /\  ps ) )
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  2040  barbari  2101  cesaro  2107  camestros  2108  calemos  2118  swopo  4228  elrnrexdm  5559  tfrcl  6261  ixpsnf1o  6630  fidcenumlemrk  6842  subhalfnqq  7229  enq0ref  7248  prarloc  7318  letrp1  8613  p1le  8614  peano2uz2  9165  uzind  9169  uzid  9347  qreccl  9441
  Copyright terms: Public domain W3C validator