MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  im2anan9 Unicode version

Theorem im2anan9 808
Description: Deduction joining nested implications to form implication of conjunctions. (Contributed by NM, 29-Feb-1996.)
Hypotheses
Ref Expression
im2an9.1  |-  ( ph  ->  ( ps  ->  ch ) )
im2an9.2  |-  ( th 
->  ( ta  ->  et ) )
Assertion
Ref Expression
im2anan9  |-  ( (
ph  /\  th )  ->  ( ( ps  /\  ta )  ->  ( ch 
/\  et ) ) )

Proof of Theorem im2anan9
StepHypRef Expression
1 im2an9.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
21adantr 451 . 2  |-  ( (
ph  /\  th )  ->  ( ps  ->  ch ) )
3 im2an9.2 . . 3  |-  ( th 
->  ( ta  ->  et ) )
43adantl 452 . 2  |-  ( (
ph  /\  th )  ->  ( ta  ->  et ) )
52, 4anim12d 546 1  |-  ( (
ph  /\  th )  ->  ( ( ps  /\  ta )  ->  ( ch 
/\  et ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  im2anan9r  809  ax11eq  2132  ax11el  2133  trin  4123  somo  4348  xpss12  4792  f1oun  5492  poxp  6227  soxp  6228  brecop  6751  ingru  8437  genpss  8628  genpnnp  8629  tgcl  16707  txlm  17342  oriso  25214  ridlideq  25335  limptlimpr2lem2  25575  lvsovso  25626  claddrvr  25648  distmlva  25688  icccon2  25700
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator