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

Theorem im2anan9 833
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 463 . 2  |-  ( (
ph  /\  th )  ->  ( ps  ->  ch ) )
3 im2an9.2 . . 3  |-  ( th 
->  ( ta  ->  et ) )
43adantl 464 . 2  |-  ( (
ph  /\  th )  ->  ( ta  ->  et ) )
52, 4anim12d 561 1  |-  ( (
ph  /\  th )  ->  ( ( ps  /\  ta )  ->  ( ch 
/\  et ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 369
This theorem is referenced by:  im2anan9r  834  ax12eq  2273  ax12el  2274  trin  4542  somo  4823  xpss12  5096  f1oun  5817  poxp  6885  soxp  6886  brecop  7396  ingru  9182  genpss  9371  genpnnp  9372  tgcl  19641  txlm  20318
  Copyright terms: Public domain W3C validator