Theorem im2anan9 876

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

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  im2anan9r  877  trin  4691  somo  4993  xpss12  5148  f1oun  6069  poxp  7176  soxp  7177  brecop  7727  ingru  9516  genpss  9705  genpnnp  9706  tgcl  20584  txlm  21261  icorempt2  32375  ax12eq  33244  ax12el  33245  31wlkdlem4  41329