Theorem 3exp2 1353

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 1352	1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

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

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 1088

This theorem is referenced by:  3anassrs  1359  pm2.61da3ne  3028  po2nr  5610  fliftfund  7332  frfi  9318  fin33i  10406  axdc3lem4  10490  iscatd  17717  isfuncd  17915  isposd  18380  pospropd  18384  imasmnd2  18799  grpinveu  19004  grpid  19005  grpasscan1  19031  imasgrp2  19085  dmdprdd  20033  pgpfac1lem5  20113  imasrng  20194  imasring  20343  islmodd  20880  lmodvsghm  20937  islssd  20950  islmhm2  21054  mulgghm2  21504  isphld  21689  riinopn  22929  ordtbaslem  23211  subbascn  23277  haust1  23375  isnrm2  23381  isnrm3  23382  lmmo  23403  nllyidm  23512  tx1stc  23673  filin  23877  filtop  23878  isfil2  23879  infil  23886  fgfil  23898  isufil2  23931  ufileu  23942  filufint  23943  flimopn  23998  flimrest  24006  isxmetd  24351  met2ndc  24551  icccmplem2  24858  lmmbr  25305  cfil3i  25316  equivcfil  25346  bcthlem5  25375  volfiniun  25595  dvidlem  25964  ulmdvlem3  26459  ax5seg  28967  axcontlem4  28996  axcont  29005  grporcan  30546  grpoinveu  30547  grpoid  30548  cvxpconn  35226  cvxsconn  35227  mclsax  35553  mclsppslem  35567  r1peuqusdeg1  35627  broutsideof2  36103  nn0prpwlem  36304  fgmin  36352  poimirlem27  37633  poimirlem29  37635  poimirlem31  37637  cntotbnd  37782  heiborlem6  37802  heiborlem10  37806  rngonegmn1l  37927  rngonegmn1r  37928  rngoneglmul  37929  rngonegrmul  37930  crngm23  37988  prnc  38053  pridlc3  38059  dmncan1  38062  lsmsat  38989  eqlkr  39080  llncmp  39504  2at0mat0  39507  llncvrlpln  39540  lplncmp  39544  lplnexllnN  39546  lplncvrlvol  39598  lvolcmp  39599  linepsubN  39734  pmapsub  39750  paddasslem16  39817  pmodlem2  39829  lhp2lt  39983  ltrneq2  40130  cdlemf2  40544  cdlemk34  40892  cdlemn11pre  41192  dihord2pre  41207  onexoegt  43232  clnbgrssedg  47764  clnbgrgrimlem  47838  grimgrtri  47851