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

Theorem anim12d 318
Description: Conjoin antecedents and consequents in a deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 18-Dec-2013.)
Hypotheses
Ref Expression
anim12d.1  |-  ( ph  ->  ( ps  ->  ch ) )
anim12d.2  |-  ( ph  ->  ( th  ->  ta ) )
Assertion
Ref Expression
anim12d  |-  ( ph  ->  ( ( ps  /\  th )  ->  ( ch  /\ 
ta ) ) )

Proof of Theorem anim12d
StepHypRef Expression
1 anim12d.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 anim12d.2 . 2  |-  ( ph  ->  ( th  ->  ta ) )
3 idd 21 . 2  |-  ( ph  ->  ( ( ch  /\  ta )  ->  ( ch 
/\  ta ) ) )
41, 2, 3syl2and 279 1  |-  ( ph  ->  ( ( ps  /\  th )  ->  ( ch  /\ 
ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  anim1d  319  anim2d  320  prth  326  im2anan9  530  anim12dan  532  3anim123d  1214  hband  1378  hbbid  1467  spsbim  1724  moim  1964  moimv  1966  2euswapdc  1991  rspcimedv  2658  soss  4051  trin2  4716  xp11m  4759  funss  4920  fun  5063  dff13  5407  f1eqcocnv  5431  isores3  5455  isosolem  5463  f1o2ndf1  5849  tposfn2  5881  tposf1o2  5885  nnaordex  6100  recexprlemss1l  6733  recexprlemss1u  6734  caucvgsrlemoffres  6884  nnindnn  6967  lemul12b  7827  lt2msq  7852  cju  7913  nnind  7930  uz11  8495  xrre2  8734
  Copyright terms: Public domain W3C validator