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  808  trin  5270  somo  5630  xpss12  5699  f1oun  6866  poxp  8154  soxp  8155  brecop  8851  dfac5lem4  10167  ingru  10856  genpss  11045  genpnnp  11046  tgcl  22977  txlm  23657  upgrpredgv  29157  3wlkdlem4  30182  frgrwopreglem5  30341  frgrwopreglem5ALT  30342  icorempo  37353  ax12eq  38943  ax12el  38944  odd2prm2  47710
  Copyright terms: Public domain W3C validator