Theorem 3anim123d 1360

Description: Deduction joining 3 implications to form implication of conjunctions. (Contributed by NM, 24-Feb-2005.)

Hypotheses

Ref	Expression
3anim123d.1	⊢ (𝜑 → (𝜓 → 𝜒))
3anim123d.2	⊢ (𝜑 → (𝜃 → 𝜏))
3anim123d.3	⊢ (𝜑 → (𝜂 → 𝜁))

Assertion

Ref	Expression
3anim123d	⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) → (𝜒 ∧ 𝜏 ∧ 𝜁)))

Proof of Theorem 3anim123d

Step	Hyp	Ref	Expression
1		3anim123d.1	. . . 4 ⊢ (𝜑 → (𝜓 → 𝜒))
2		3anim123d.2	. . . 4 ⊢ (𝜑 → (𝜃 → 𝜏))
3	1, 2	anim12d 335	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜏)))
4		3anim123d.3	. . 3 ⊢ (𝜑 → (𝜂 → 𝜁))
5	3, 4	anim12d 335	. 2 ⊢ (𝜑 → (((𝜓 ∧ 𝜃) ∧ 𝜂) → ((𝜒 ∧ 𝜏) ∧ 𝜁)))
6		df-3an 1011	. 2 ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ ((𝜓 ∧ 𝜃) ∧ 𝜂))
7		df-3an 1011	. 2 ⊢ ((𝜒 ∧ 𝜏 ∧ 𝜁) ↔ ((𝜒 ∧ 𝜏) ∧ 𝜁))
8	5, 6, 7	3imtr4g 205	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) → (𝜒 ∧ 𝜏 ∧ 𝜁)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  hb3and  1543  pofun  4457  soss  4459  wessep  4725  isopolem  6028  isosolem  6030  issmo2  6560  smores  6563  issubmnd  13757  issubg2m  13994  issubrng2  14520  issubrg2  14551  rnglidlmsgrp  14836  rnglidlrng  14837  issubassa3  15014  sslm  15350