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  5612  dff14i  7193  ovg  7511  fisup2g  9353  fiinf2g  9386  cfcoflem  10163  ttukeylem5  10404  dedekindle  11277  grplcan  18913  mulgnnass  19022  dmdprdsplit2  19961  mulgass2  20228  lmodvsdi  20819  lmodvsdir  20820  lmodvsass  20821  lss1d  20897  islmhm2  20973  lspsolvlem  21080  lbsextlem2  21097  cygznlem2a  21505  isphld  21592  t0dist  23241  hausnei  23244  nrmsep3  23271  fclsopni  23931  fcfneii  23953  ax5seglem5  28912  axcont  28955  grporcan  30496  grpolcan  30508  slmdvsdi  33182  slmdvsdir  33183  slmdvsass  33184  elrspunidl  33391  zarcmplem  33892  mclsppslem  35625  broutsideof2  36162  poimirlem31  37697  broucube  37700  frinfm  37781  crngm23  38048  pridl  38083  pridlc  38117  dmnnzd  38121  dmncan1  38122  paddasslem5  39869  or2expropbi  47071  elsetpreimafveqfv  47429  sfprmdvdsmersenne  47640  isgrtri  47980  grlimprclnbgr  48033