Theorem 3imp1 1348

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  1360  reupick2  4281  indcardi  9949  ledivge1le  12976  expcan  14090  ltexp2  14091  leexp1a  14096  expnbnd  14153  cshf1  14731  rtrclreclem4  14982  relexpindlem  14984  ncoprmlnprm  16653  rnglidlmcl  21169  xrsdsreclblem  21365  matecl  22367  scmateALT  22454  riinopn  22850  neindisj2  23065  filufint  23862  tsmsxp  24097  ewlkle  29628  uspgr2wlkeq  29668  spthonepeq  29774  wwlksm1edg  29903  clwwisshclwws  30039  clwwlknwwlksn  30062  clwwlkinwwlk  30064  wwlksext2clwwlk  30081  3vfriswmgr  30302  homco1  31825  homulass  31826  hoadddir  31828  satffunlem  35544  mblfinlem3  37799  zerdivemp1x  38087  athgt  39655  psubspi  39946  paddasslem14  40032  eluzge0nn0  47500  iccpartigtl  47611  lighneal  47799  uhgrimisgrgriclem  48118  uhgrimisgrgric  48119  clnbgrgrimlem  48121  uspgrlimlem3  48178  clnbgr3stgrgrlic  48208  gpgusgralem  48244