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  1765  ssel  2994  sscon  3107  uniss  3630  trel3  3891  copsexg  4007  ssopab2  4038  coss1  4519  fununi  4998  imadif  5010  fss  5085  ssimaex  5266  opabbrex  5580  ssoprab2  5592  poxp  5884  xpdom2  6375  qbtwnxr  9344  ioc0  9349  climshftlemg  10279  bezoutlembz  10537
  Copyright terms: Public domain W3C validator