Theorem 3imp2 1368

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 1367	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏))
3	2	imp 412	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  wereu  5646  dff14i  7264  ovg  7586  fisup2g  9465  fiinf2g  9498  cfcoflem  10354  ttukeylem5  10595  dedekindle  11478  grplcan  19217  mulgnnass  19325  dmdprdsplit2  20268  mulgass2  20546  lmodvsdi  21166  lmodvsdir  21167  lmodvsass  21168  lss1d  21244  islmhm2  21319  lspsolvlem  21426  lbsextlem2  21443  unichnlidl  21522  cygznlem2a  21879  isphld  21966  t0dist  23649  hausnei  23652  nrmsep3  23679  fclsopni  24340  fcfneii  24362  ax5seglem5  29517  axcont  29560  grporcan  31126  grpolcan  31138  slmdvsdi  33823  slmdvsdir  33824  slmdvsass  33825  zarcmplem  34560  mclsppslem  36435  broutsideof2  36980  poimirlem31  38663  broucube  38666  frinfm  38763  crngm23  39030  pridl  39065  pridlc  39099  dmnnzd  39103  dmncan1  39104  paddasslem5  40975  or2expropbi  48198  elsetpreimafveqfv  48568  sfprmdvdsmersenne  48782  isgrtri  49135  grlimprclnbgr  49188  idomnzd  49537  idomcanl  49538