Theorem im2anan9 621

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  im2anan9r  622  anim12  809  mo4  2566  trin  5204  somo  5578  xpss12  5646  f1oun  6799  poxp  8078  soxp  8079  brecop  8757  dfac5lem4  10048  ingru  10738  genpss  10927  genpnnp  10928  tgcl  22934  txlm  23613  upgrpredgv  29208  3wlkdlem4  30232  frgrwopreglem5  30391  frgrwopreglem5ALT  30392  icorempo  37667  ax12eq  39387  ax12el  39388  odd2prm2  48194