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

Theorem im2anan9 853
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 472 . 2  |-  ( (
ph  /\  th )  ->  ( ps  ->  ch ) )
3 im2an9.2 . . 3  |-  ( th 
->  ( ta  ->  et ) )
43adantl 473 . 2  |-  ( (
ph  /\  th )  ->  ( ta  ->  et ) )
52, 4anim12d 572 1  |-  ( (
ph  /\  th )  ->  ( ( ps  /\  ta )  ->  ( ch 
/\  et ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 376
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 190  df-an 378
This theorem is referenced by:  im2anan9r  854  trin  4500  somo  4794  xpss12  4945  f1oun  5847  poxp  6927  soxp  6928  brecop  7474  ingru  9258  genpss  9447  genpnnp  9448  tgcl  20062  txlm  20740  icorempt2  31824  ax12eq  32576  ax12el  32577  31wlkdlem4  40076
  Copyright terms: Public domain W3C validator