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

Theorem ancli 316
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 300 1  |-  ( ph  ->  ( ph  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106
This theorem is referenced by:  pm4.45im  327  mo23  1983  barbari  2044  cesaro  2050  camestros  2051  calemos  2061  swopo  4069  elrnrexdm  5338  tfrcl  6013  subhalfnqq  6666  enq0ref  6685  prarloc  6755  letrp1  7993  p1le  7994  peano2uz2  8535  uzind  8539  uzid  8714  qreccl  8808
  Copyright terms: Public domain W3C validator