Theorem 3imp2 1350

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 1349	. 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:  wereu  5650  dff14i  7252  ovg  7572  fisup2g  9481  fiinf2g  9514  cfcoflem  10286  ttukeylem5  10527  dedekindle  11399  grplcan  18983  mulgnnass  19092  dmdprdsplit2  20029  mulgass2  20269  lmodvsdi  20842  lmodvsdir  20843  lmodvsass  20844  lss1d  20920  islmhm2  20996  lspsolvlem  21103  lbsextlem2  21120  cygznlem2a  21528  isphld  21614  t0dist  23263  hausnei  23266  nrmsep3  23293  fclsopni  23953  fcfneii  23975  ax5seglem5  28912  axcont  28955  grporcan  30499  grpolcan  30511  slmdvsdi  33212  slmdvsdir  33213  slmdvsass  33214  elrspunidl  33443  zarcmplem  33912  mclsppslem  35605  broutsideof2  36140  poimirlem31  37675  broucube  37678  frinfm  37759  crngm23  38026  pridl  38061  pridlc  38095  dmnnzd  38099  dmncan1  38100  paddasslem5  39843  or2expropbi  47063  elsetpreimafveqfv  47406  sfprmdvdsmersenne  47617  isgrtri  47955