Theorem im2anan9 632

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 497	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜏) → 𝜒))
3		im2an9.2	. . 3 ⊢ (𝜃 → (𝜏 → 𝜂))
4	3	adantld 496	. 2 ⊢ (𝜃 → ((𝜓 ∧ 𝜏) → 𝜂))
5	2, 4	anim12ii 630	1 ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ∧ 𝜏) → (𝜒 ∧ 𝜂)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  im2anan9r  633  anim12  821  mo4  2591  trin  5223  somo  5597  xpss12  5665  f1oun  6845  poxp  8143  soxp  8144  brecop  8835  dfac5lem4  10209  ingru  10904  genpss  11093  genpnnp  11094  tgcl  23293  txlm  23973  upgrpredgv  29723  3wlkdlem4  30769  frgrwopreglem5  30928  frgrwopreglem5ALT  30929  acwer1prclem  35816  icorempo  38368  ax12eq  40092  ax12el  40093  odd2prm2  48910