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  5224  somo  5602  xpss12  5670  f1oun  6837  poxp  8126  soxp  8127  brecop  8810  dfac5lem4  10129  ingru  10824  genpss  11013  genpnnp  11014  tgcl  23194  txlm  23874  upgrpredgv  29596  3wlkdlem4  30642  frgrwopreglem5  30801  frgrwopreglem5ALT  30802  icorempo  38105  ax12eq  39814  ax12el  39815  odd2prm2  48634