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

Theorem im2anan9 620
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 (𝜑 → (𝜓𝜒))
21adantrd 492 . 2 (𝜑 → ((𝜓𝜏) → 𝜒))
3 im2an9.2 . . 3 (𝜃 → (𝜏𝜂))
43adantld 491 . 2 (𝜃 → ((𝜓𝜏) → 𝜂))
52, 4anim12ii 618 1 ((𝜑𝜃) → ((𝜓𝜏) → (𝜒𝜂)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 206  df-an 397
This theorem is referenced by:  im2anan9r  621  anim12  807  trin  5277  somo  5625  xpss12  5691  f1oun  6852  poxp  8116  soxp  8117  brecop  8806  ingru  10812  genpss  11001  genpnnp  11002  tgcl  22479  txlm  23159  upgrpredgv  28437  3wlkdlem4  29453  frgrwopreglem5  29612  frgrwopreglem5ALT  29613  icorempo  36318  ax12eq  37897  ax12el  37898  odd2prm2  46465
  Copyright terms: Public domain W3C validator