Theorem im2anan9 898

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 585	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 197  df-an 385

This theorem is referenced by:  im2anan9r  899  trin  4796  somo  5098  xpss12  5158  f1oun  6194  poxp  7334  soxp  7335  brecop  7883  ingru  9675  genpss  9864  genpnnp  9865  tgcl  20821  txlm  21499  upgrpredgv  26079  3wlkdlem4  27140  frgrwopreglem5  27301  frgrwopreglem5ALT  27302  icorempt2  33329  ax12eq  34545  ax12el  34546  odd2prm2  41952