Theorem 3exp2 1356

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 1355	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:  3anassrs  1362  pm2.61da3ne  3022  po2nr  5546  fliftfund  7261  frfi  9188  fin33i  10282  axdc3lem4  10366  iscatd  17630  isfuncd  17823  isposd  18279  pospropd  18282  imasmnd2  18733  grpinveu  18941  grpid  18942  grpasscan1  18968  imasgrp2  19022  dmdprdd  19967  pgpfac1lem5  20047  imasrng  20149  imasring  20301  islmodd  20852  lmodvsghm  20909  islssd  20921  islmhm2  21025  mulgghm2  21466  isphld  21644  riinopn  22883  ordtbaslem  23163  subbascn  23229  haust1  23327  isnrm2  23333  isnrm3  23334  lmmo  23355  nllyidm  23464  tx1stc  23625  filin  23829  filtop  23830  isfil2  23831  infil  23838  fgfil  23850  isufil2  23883  ufileu  23894  filufint  23895  flimopn  23950  flimrest  23958  isxmetd  24301  met2ndc  24498  icccmplem2  24799  lmmbr  25235  cfil3i  25246  equivcfil  25276  bcthlem5  25305  volfiniun  25524  dvidlem  25892  ulmdvlem3  26380  ax5seg  29021  axcontlem4  29050  axcont  29059  grporcan  30604  grpoinveu  30605  grpoid  30606  cvxpconn  35440  cvxsconn  35441  mclsax  35767  mclsppslem  35781  r1peuqusdeg1  35841  broutsideof2  36320  nn0prpwlem  36520  fgmin  36568  poimirlem27  37982  poimirlem29  37984  poimirlem31  37986  cntotbnd  38131  heiborlem6  38151  heiborlem10  38155  rngonegmn1l  38276  rngonegmn1r  38277  rngoneglmul  38278  rngonegrmul  38279  crngm23  38337  prnc  38402  pridlc3  38408  dmncan1  38411  lsmsat  39468  eqlkr  39559  llncmp  39982  2at0mat0  39985  llncvrlpln  40018  lplncmp  40022  lplnexllnN  40024  lplncvrlvol  40076  lvolcmp  40077  linepsubN  40212  pmapsub  40228  paddasslem16  40295  pmodlem2  40307  lhp2lt  40461  ltrneq2  40608  cdlemf2  41022  cdlemk34  41370  cdlemn11pre  41670  dihord2pre  41685  onexoegt  43690  clnbgrssedg  48329  clnbgrgrimlem  48421  grimgrtri  48437