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 465 . 2  |-  ( (
ph  /\  th )  ->  ( ps  ->  ch ) )
3 im2an9.2 . . 3  |-  ( th 
->  ( ta  ->  et ) )
43adantl 466 . 2  |-  ( (
ph  /\  th )  ->  ( ta  ->  et ) )
52, 4anim12d 563 1  |-  ( (
ph  /\  th )  ->  ( ( ps  /\  ta )  ->  ( ch 
/\  et ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 371
This theorem is referenced by:  im2anan9r  834  ax12eq  2264  ax12el  2265  trin  4555  somo  4839  xpss12  5113  f1oun  5840  poxp  6905  soxp  6906  brecop  7414  ingru  9203  genpss  9392  genpnnp  9393  tgcl  19316  txlm  19994
  Copyright terms: Public domain W3C validator