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  2559  trin  5226  somo  5585  xpss12  5653  f1oun  6819  poxp  8107  soxp  8108  brecop  8783  dfac5lem4  10079  ingru  10768  genpss  10957  genpnnp  10958  tgcl  22856  txlm  23535  upgrpredgv  29066  3wlkdlem4  30091  frgrwopreglem5  30250  frgrwopreglem5ALT  30251  icorempo  37339  ax12eq  38934  ax12el  38935  odd2prm2  47719