Theorem im2anan9 610

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	adantr 473	. 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 → 𝜒))
3		im2an9.2	. . 3 ⊢ (𝜃 → (𝜏 → 𝜂))
4	3	adantl 474	. 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜏 → 𝜂))
5	2, 4	anim12d 599	1 ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ∧ 𝜏) → (𝜒 ∧ 𝜂)))

Syntax hints:   → wi 4   ∧ wa 387

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 199  df-an 388

This theorem is referenced by:  im2anan9r  611  trin  5038  somo  5359  xpss12  5419  f1oun  6461  poxp  7624  soxp  7625  brecop  8186  ingru  10031  genpss  10220  genpnnp  10221  tgcl  21275  txlm  21954  upgrpredgv  26621  3wlkdlem4  27685  frgrwopreglem5  27849  frgrwopreglem5ALT  27850  icorempt2  34039  ax12eq  35500  ax12el  35501  odd2prm2  43225