Theorem 3exp2 1373

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  3anassrs  1381  pm2.61da3ne  3047  po2nr  5585  fliftfund  7313  frfi  9246  fin33i  10354  axdc3lem4  10438  iscatd  17730  isfuncd  17923  isposd  18379  pospropd  18382  imasmnd2  18833  grpinveu  19042  grpid  19043  grpasscan1  19069  imasgrp2  19122  dmdprdd  20072  pgpfac1lem5  20152  imasrng  20256  imasring  20413  islmodd  20968  lmodvsghm  21025  islssd  21037  islmhm2  21140  cmprmidlmcl  21456  mulgghm2  21607  isphld  21785  riinopn  23046  ordtbaslem  23326  subbascn  23392  haust1  23490  isnrm2  23496  isnrm3  23497  lmmo  23518  nllyidm  23627  tx1stc  23788  filin  23992  filtop  23993  isfil2  23994  infil  24001  fgfil  24013  isufil2  24046  ufileu  24057  filufint  24058  flimopn  24113  flimrest  24121  isxmetd  24464  met2ndc  24661  icccmplem2  24962  lmmbr  25398  cfil3i  25409  equivcfil  25439  bcthlem5  25468  volfiniun  25687  dvidlem  26055  ulmdvlem3  26546  ax5seg  29269  axcontlem4  29298  axcont  29307  grporcan  30851  grpoinveu  30852  grpoid  30853  cvxpconn  35715  cvxsconn  35716  mclsax  36042  mclsppslem  36056  r1peuqusdeg1  36116  broutsideof2  36595  nn0prpwlem  36814  fgmin  36862  poimirlem27  38279  poimirlem29  38281  poimirlem31  38283  cntotbnd  38428  heiborlem6  38448  heiborlem10  38452  rngonegmn1l  38573  rngonegmn1r  38574  rngoneglmul  38575  rngonegrmul  38576  crngm23  38634  prnc  38699  pridlc3  38705  dmncan1  38708  lsmsat  39763  eqlkr  39854  llncmp  40277  2at0mat0  40280  llncvrlpln  40313  lplncmp  40317  lplnexllnN  40319  lplncvrlvol  40371  lvolcmp  40372  linepsubN  40507  pmapsub  40523  paddasslem16  40590  pmodlem2  40602  lhp2lt  40756  ltrneq2  40903  cdlemf2  41317  cdlemk34  41665  cdlemn11pre  41965  dihord2pre  41980  onexoegt  43954  clnbgrssedg  48589  clnbgrgrimlem  48681  grimgrtri  48697  idomcanl  49095