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

Theorem anim2d 330
Description: Add a conjunct to left of antecedent and consequent in a deduction. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
anim1d.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
anim2d  |-  ( ph  ->  ( ( th  /\  ps )  ->  ( th 
/\  ch ) ) )

Proof of Theorem anim2d
StepHypRef Expression
1 idd 21 . 2  |-  ( ph  ->  ( th  ->  th )
)
2 anim1d.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2anim12d 328 1  |-  ( ph  ->  ( ( th  /\  ps )  ->  ( th 
/\  ch ) ) )
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-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  spsbim  1768  ssel  3008  sscon  3123  uniss  3659  trel3  3921  copsexg  4047  ssopab2  4078  coss1  4561  fununi  5049  imadif  5061  fss  5138  ssimaex  5330  opabbrex  5652  ssoprab2  5664  poxp  5956  pmss12g  6386  xpdom2  6501  qbtwnxr  9600  ioc0  9605  climshftlemg  10588  bezoutlembz  10899
  Copyright terms: Public domain W3C validator