Theorem 3imp1 1346

Description: Importation to left triple conjunction. (Contributed by NM, 24-Feb-2005.)

Hypothesis

Ref	Expression
3imp1.1	⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Assertion

Ref	Expression
3imp1	⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)

Proof of Theorem 3imp1

Step	Hyp	Ref	Expression
1		3imp1.1	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
2	1	3imp 1110	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 → 𝜏))
3	2	imp 406	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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  df-3an 1088

This theorem is referenced by:  3an1rs  1358  reupick2  4336  indcardi  10078  ledivge1le  13103  expcan  14205  ltexp2  14206  leexp1a  14211  expnbnd  14267  cshf1  14844  rtrclreclem4  15096  relexpindlem  15098  ncoprmlnprm  16761  rnglidlmcl  21243  xrsdsreclblem  21447  matecl  22446  scmateALT  22533  riinopn  22929  neindisj2  23146  filufint  23943  tsmsxp  24178  ewlkle  29637  uspgr2wlkeq  29678  spthonepeq  29784  wwlksm1edg  29910  clwwisshclwws  30043  clwwlknwwlksn  30066  clwwlkinwwlk  30068  wwlksext2clwwlk  30085  3vfriswmgr  30306  homco1  31829  homulass  31830  hoadddir  31832  satffunlem  35385  mblfinlem3  37645  zerdivemp1x  37933  athgt  39438  psubspi  39729  paddasslem14  39815  eluzge0nn0  47261  iccpartigtl  47347  lighneal  47535  uhgrimisgrgriclem  47835  uhgrimisgrgric  47836  clnbgrgrimlem  47838  uspgrlimlem3  47892  clnbgr3stgrgrlic  47914  gpgusgralem  47945