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

Theorem anim2d 337
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 335 1  |-  ( ph  ->  ( ( th  /\  ps )  ->  ( th 
/\  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  spsbim  1843  ssel  3149  sscon  3269  uniss  3828  trel3  4106  copsexg  4240  ssopab2  4271  coss1  4777  fununi  5279  imadif  5291  fss  5372  ssimaex  5572  opabbrex  5912  ssoprab2  5924  poxp  6226  pmss12g  6668  ss2ixp  6704  xpdom2  6824  qbtwnxr  10231  ioc0  10236  climshftlemg  11281  bezoutlembz  11975  tgcl  13197  neipsm  13287  ssnei2  13290  tgcnp  13342  cnpnei  13352  cnptopco  13355  mopni3  13617  limcresi  13768  cnlimcim  13773
  Copyright terms: Public domain W3C validator