Theorem 3exp2 1307

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 449	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏))
3	2	3expd 1306	1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

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

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 197  df-an 385  df-3an 1056

This theorem is referenced by:  3anassrs  1313  pm2.61da3ne  2912  po2nr  5077  predpo  5736  fliftfund  6603  frfi  8246  fin33i  9229  axdc3lem4  9313  relexpaddd  13838  iscatd  16381  isfuncd  16572  isposd  17002  pospropd  17181  imasmnd2  17374  grpinveu  17503  grpid  17504  grpasscan1  17525  imasgrp2  17577  dmdprdd  18444  pgpfac1lem5  18524  imasring  18665  islmodd  18917  lmodvsghm  18972  islssd  18984  islmhm2  19086  psrbaglefi  19420  mulgghm2  19893  isphld  20047  riinopn  20761  ordtbaslem  21040  subbascn  21106  haust1  21204  isnrm2  21210  isnrm3  21211  lmmo  21232  nllyidm  21340  tx1stc  21501  filin  21705  filtop  21706  isfil2  21707  infil  21714  fgfil  21726  isufil2  21759  ufileu  21770  filufint  21771  flimopn  21826  flimrest  21834  isxmetd  22178  met2ndc  22375  icccmplem2  22673  lmmbr  23102  cfil3i  23113  equivcfil  23143  bcthlem5  23171  volfiniun  23361  dvidlem  23724  ulmdvlem3  24201  ax5seg  25863  axcontlem4  25892  axcont  25901  grporcan  27500  grpoinveu  27501  grpoid  27502  cvxpconn  31350  cvxsconn  31351  mclsax  31592  mclsppslem  31606  broutsideof2  32354  nn0prpwlem  32442  fgmin  32490  poimirlem27  33566  poimirlem29  33568  poimirlem31  33570  cntotbnd  33725  heiborlem6  33745  heiborlem10  33749  rngonegmn1l  33870  rngonegmn1r  33871  rngoneglmul  33872  rngonegrmul  33873  crngm23  33931  prnc  33996  pridlc3  34002  dmncan1  34005  lsmsat  34613  eqlkr  34704  llncmp  35126  2at0mat0  35129  llncvrlpln  35162  lplncmp  35166  lplnexllnN  35168  lplncvrlvol  35220  lvolcmp  35221  linepsubN  35356  pmapsub  35372  paddasslem16  35439  pmodlem2  35451  lhp2lt  35605  ltrneq2  35752  cdlemf2  36167  cdlemk34  36515  cdlemn11pre  36816  dihord2pre  36831