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

Theorem im2anan9 622
 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 495 . 2 (𝜑 → ((𝜓𝜏) → 𝜒))
3 im2an9.2 . . 3 (𝜃 → (𝜏𝜂))
43adantld 494 . 2 (𝜃 → ((𝜓𝜏) → 𝜂))
52, 4anim12ii 620 1 ((𝜑𝜃) → ((𝜓𝜏) → (𝜒𝜂)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399 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 210  df-an 400 This theorem is referenced by:  im2anan9r  623  anim12  808  trin  5148  somo  5479  xpss12  5539  f1oun  6621  poxp  7827  soxp  7828  brecop  8400  ingru  10275  genpss  10464  genpnnp  10465  tgcl  21669  txlm  22348  upgrpredgv  27031  3wlkdlem4  28046  frgrwopreglem5  28205  frgrwopreglem5ALT  28206  icorempo  35048  ax12eq  36517  ax12el  36518  odd2prm2  44603
 Copyright terms: Public domain W3C validator