Theorem 3exp2 1355

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 1354	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  1361  pm2.61da3ne  3031  po2nr  5606  fliftfund  7333  frfi  9321  fin33i  10409  axdc3lem4  10493  iscatd  17716  isfuncd  17910  isposd  18368  pospropd  18372  imasmnd2  18787  grpinveu  18992  grpid  18993  grpasscan1  19019  imasgrp2  19073  dmdprdd  20019  pgpfac1lem5  20099  imasrng  20174  imasring  20327  islmodd  20864  lmodvsghm  20921  islssd  20933  islmhm2  21037  mulgghm2  21487  isphld  21672  riinopn  22914  ordtbaslem  23196  subbascn  23262  haust1  23360  isnrm2  23366  isnrm3  23367  lmmo  23388  nllyidm  23497  tx1stc  23658  filin  23862  filtop  23863  isfil2  23864  infil  23871  fgfil  23883  isufil2  23916  ufileu  23927  filufint  23928  flimopn  23983  flimrest  23991  isxmetd  24336  met2ndc  24536  icccmplem2  24845  lmmbr  25292  cfil3i  25303  equivcfil  25333  bcthlem5  25362  volfiniun  25582  dvidlem  25950  ulmdvlem3  26445  ax5seg  28953  axcontlem4  28982  axcont  28991  grporcan  30537  grpoinveu  30538  grpoid  30539  cvxpconn  35247  cvxsconn  35248  mclsax  35574  mclsppslem  35588  r1peuqusdeg1  35648  broutsideof2  36123  nn0prpwlem  36323  fgmin  36371  poimirlem27  37654  poimirlem29  37656  poimirlem31  37658  cntotbnd  37803  heiborlem6  37823  heiborlem10  37827  rngonegmn1l  37948  rngonegmn1r  37949  rngoneglmul  37950  rngonegrmul  37951  crngm23  38009  prnc  38074  pridlc3  38080  dmncan1  38083  lsmsat  39009  eqlkr  39100  llncmp  39524  2at0mat0  39527  llncvrlpln  39560  lplncmp  39564  lplnexllnN  39566  lplncvrlvol  39618  lvolcmp  39619  linepsubN  39754  pmapsub  39770  paddasslem16  39837  pmodlem2  39849  lhp2lt  40003  ltrneq2  40150  cdlemf2  40564  cdlemk34  40912  cdlemn11pre  41212  dihord2pre  41227  onexoegt  43256  clnbgrssedg  47827  clnbgrgrimlem  47901  grimgrtri  47916