Theorem 3imp2 1351

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  wereu  5627  dff14i  7214  ovg  7532  fisup2g  9382  fiinf2g  9415  cfcoflem  10194  ttukeylem5  10435  dedekindle  11310  grplcan  18976  mulgnnass  19085  dmdprdsplit2  20023  mulgass2  20290  lmodvsdi  20880  lmodvsdir  20881  lmodvsass  20882  lss1d  20958  islmhm2  21033  lspsolvlem  21140  lbsextlem2  21157  cygznlem2a  21547  isphld  21634  t0dist  23290  hausnei  23293  nrmsep3  23320  fclsopni  23980  fcfneii  24002  ax5seglem5  29002  axcont  29045  grporcan  30589  grpolcan  30601  slmdvsdi  33276  slmdvsdir  33277  slmdvsass  33278  elrspunidl  33488  zarcmplem  34025  mclsppslem  35765  broutsideof2  36304  poimirlem31  37972  broucube  37975  frinfm  38056  crngm23  38323  pridl  38358  pridlc  38392  dmnnzd  38396  dmncan1  38397  paddasslem5  40270  or2expropbi  47482  elsetpreimafveqfv  47852  sfprmdvdsmersenne  48066  isgrtri  48419  grlimprclnbgr  48472