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

Theorem im2anan9 875
Description: Deduction joining nested implications to form implication of conjunctions. (Contributed by NM, 29-Feb-1996.)
Hypotheses
Ref Expression
im2an9.1 (𝜑 → (𝜓𝜒))
im2an9.2 (𝜃 → (𝜏𝜂))
Assertion
Ref Expression
im2anan9 ((𝜑𝜃) → ((𝜓𝜏) → (𝜒𝜂)))

Proof of Theorem im2anan9
StepHypRef Expression
1 im2an9.1 . . 3 (𝜑 → (𝜓𝜒))
21adantr 479 . 2 ((𝜑𝜃) → (𝜓𝜒))
3 im2an9.2 . . 3 (𝜃 → (𝜏𝜂))
43adantl 480 . 2 ((𝜑𝜃) → (𝜏𝜂))
52, 4anim12d 583 1 ((𝜑𝜃) → ((𝜓𝜏) → (𝜒𝜂)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  im2anan9r  876  trin  4685  somo  4983  xpss12  5137  f1oun  6054  poxp  7153  soxp  7154  brecop  7704  ingru  9493  genpss  9682  genpnnp  9683  tgcl  20526  txlm  21203  icorempt2  32178  ax12eq  33047  ax12el  33048  31wlkdlem4  41331
  Copyright terms: Public domain W3C validator