Theorem 3exp2 1352

Description: Exportation from right triple conjunction. (Contributed by NM, 26-Oct-2006.)

Hypothesis

Ref	Expression
3exp2.1	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏)

Assertion

Ref	Expression
3exp2	⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Proof of Theorem 3exp2

Step	Hyp	Ref	Expression
1		3exp2.1	. . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏)
2	1	ex 412	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏))
3	2	3expd 1351	1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

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

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  3anassrs  1358  pm2.61da3ne  3032  po2nr  5513  fliftfund  7169  frfi  9005  fin33i  10072  axdc3lem4  10156  iscatd  17326  isfuncd  17524  isposd  17985  pospropd  17989  imasmnd2  18366  grpinveu  18558  grpid  18559  grpasscan1  18582  imasgrp2  18634  dmdprdd  19546  pgpfac1lem5  19626  imasring  19802  islmodd  20073  lmodvsghm  20128  islssd  20141  islmhm2  20244  mulgghm2  20642  isphld  20803  psrbaglefiOLD  21080  riinopn  22001  ordtbaslem  22283  subbascn  22349  haust1  22447  isnrm2  22453  isnrm3  22454  lmmo  22475  nllyidm  22584  tx1stc  22745  filin  22949  filtop  22950  isfil2  22951  infil  22958  fgfil  22970  isufil2  23003  ufileu  23014  filufint  23015  flimopn  23070  flimrest  23078  isxmetd  23423  met2ndc  23623  icccmplem2  23930  lmmbr  24365  cfil3i  24376  equivcfil  24406  bcthlem5  24435  volfiniun  24654  dvidlem  25022  ulmdvlem3  25504  ax5seg  27249  axcontlem4  27278  axcont  27287  grporcan  28821  grpoinveu  28822  grpoid  28823  cvxpconn  33146  cvxsconn  33147  mclsax  33473  mclsppslem  33487  broutsideof2  34393  nn0prpwlem  34480  fgmin  34528  poimirlem27  35773  poimirlem29  35775  poimirlem31  35777  cntotbnd  35923  heiborlem6  35943  heiborlem10  35947  rngonegmn1l  36068  rngonegmn1r  36069  rngoneglmul  36070  rngonegrmul  36071  crngm23  36129  prnc  36194  pridlc3  36200  dmncan1  36203  lsmsat  36991  eqlkr  37082  llncmp  37505  2at0mat0  37508  llncvrlpln  37541  lplncmp  37545  lplnexllnN  37547  lplncvrlvol  37599  lvolcmp  37600  linepsubN  37735  pmapsub  37751  paddasslem16  37818  pmodlem2  37830  lhp2lt  37984  ltrneq2  38131  cdlemf2  38545  cdlemk34  38893  cdlemn11pre  39193  dihord2pre  39208