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

Step	Hyp	Ref	Expression
1		im2an9.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	adantrd 491	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜏) → 𝜒))
3		im2an9.2	. . 3 ⊢ (𝜃 → (𝜏 → 𝜂))
4	3	adantld 490	. 2 ⊢ (𝜃 → ((𝜓 ∧ 𝜏) → 𝜂))
5	2, 4	anim12ii 618	1 ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ∧ 𝜏) → (𝜒 ∧ 𝜂)))

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  mo4  2560  trin  5229  somo  5588  xpss12  5656  f1oun  6822  poxp  8110  soxp  8111  brecop  8786  dfac5lem4  10086  ingru  10775  genpss  10964  genpnnp  10965  tgcl  22863  txlm  23542  upgrpredgv  29073  3wlkdlem4  30098  frgrwopreglem5  30257  frgrwopreglem5ALT  30258  icorempo  37346  ax12eq  38941  ax12el  38942  odd2prm2  47723