Theorem 3imp2 1356

Description: Importation to right triple conjunction. (Contributed by NM, 26-Oct-2006.)

Hypothesis

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

Assertion

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

Proof of Theorem 3imp2

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  wereu  5621  dff14i  7210  ovg  7528  fisup2g  9379  fiinf2g  9412  cfcoflem  10192  ttukeylem5  10433  dedekindle  11308  grplcan  18974  mulgnnass  19083  dmdprdsplit2  20021  mulgass2  20288  lmodvsdi  20882  lmodvsdir  20883  lmodvsass  20884  lss1d  20960  islmhm2  21035  lspsolvlem  21142  lbsextlem2  21159  cygznlem2a  21549  isphld  21636  t0dist  23315  hausnei  23318  nrmsep3  23345  fclsopni  24005  fcfneii  24027  ax5seglem5  29027  axcont  29070  grporcan  30614  grpolcan  30626  slmdvsdi  33303  slmdvsdir  33304  slmdvsass  33305  elrspunidl  33518  zarcmplem  34072  mclsppslem  35818  broutsideof2  36357  poimirlem31  38025  broucube  38028  frinfm  38109  crngm23  38376  pridl  38411  pridlc  38445  dmnnzd  38449  dmncan1  38450  paddasslem5  40323  or2expropbi  47504  elsetpreimafveqfv  47874  sfprmdvdsmersenne  48088  isgrtri  48441  grlimprclnbgr  48494