Theorem 3imp2 1274

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  wereu  5034  ovg  6697  fisup2g  8257  fiinf2g  8289  cfcoflem  8977  ttukeylem5  9218  dedekindle  10080  grplcan  17300  mulgnnass  17399  mulgnnassOLD  17400  dmdprdsplit2  18268  mulgass2  18424  lmodvsdi  18709  lmodvsdir  18710  lmodvsass  18711  lss1d  18784  islmhm2  18859  lspsolvlem  18963  lbsextlem2  18980  cygznlem2a  19735  isphld  19818  t0dist  20939  hausnei  20942  nrmsep3  20969  fclsopni  21629  fcfneii  21651  ax5seglem5  25613  axcont  25656  grporcan  26756  grpolcan  26768  slmdvsdi  29099  slmdvsdir  29100  slmdvsass  29101  mclsppslem  30734  broutsideof2  31399  poimirlem31  32610  broucube  32613  frinfm  32700  crngm23  32971  pridl  33006  pridlc  33040  dmnnzd  33044  dmncan1  33045  paddasslem5  34128  sfprmdvdsmersenne  40058