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 491 . 2 (𝜑 → ((𝜓𝜏) → 𝜒))
3 im2an9.2 . . 3 (𝜃 → (𝜏𝜂))
43adantld 490 . 2 (𝜃 → ((𝜓𝜏) → 𝜂))
52, 4anim12ii 618 1 ((𝜑𝜃) → ((𝜓𝜏) → (𝜒𝜂)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395
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 207  df-an 396
This theorem is referenced by:  im2anan9r  621  anim12  809  trin  5277  somo  5635  xpss12  5704  f1oun  6868  poxp  8152  soxp  8153  brecop  8849  dfac5lem4  10164  ingru  10853  genpss  11042  genpnnp  11043  tgcl  22992  txlm  23672  upgrpredgv  29171  3wlkdlem4  30191  frgrwopreglem5  30350  frgrwopreglem5ALT  30351  icorempo  37334  ax12eq  38923  ax12el  38924  odd2prm2  47643
  Copyright terms: Public domain W3C validator