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

Theorem anim1d 334
Description: Add a conjunct to right of antecedent and consequent in a deduction. (Contributed by NM, 3-Apr-1994.)
Hypothesis
Ref Expression
anim1d.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
anim1d  |-  ( ph  ->  ( ( ps  /\  th )  ->  ( ch  /\ 
th ) ) )

Proof of Theorem anim1d
StepHypRef Expression
1 anim1d.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 idd 21 . 2  |-  ( ph  ->  ( th  ->  th )
)
31, 2anim12d 333 1  |-  ( ph  ->  ( ( ps  /\  th )  ->  ( ch  /\ 
th ) ) )
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-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  pm3.45  586  exdistrfor  1772  mopick2  2082  ssrexf  3159  ssrexv  3162  ssdif  3211  ssrin  3301  reupick  3360  disjss1  3912  copsexg  4166  po3nr  4232  coss2  4695  fununi  5191  fiintim  6817  recexprlemlol  7434  recexprlemupu  7436  icoshft  9773  2ffzeq  9918  qbtwnxr  10035  ico0  10039  r19.2uz  10765  bezoutlemzz  11690  bezoutlemaz  11691  neiss  12319  uptx  12443  txcn  12444
  Copyright terms: Public domain W3C validator