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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3anassrs  1381  pm2.61da3ne  3044  po2nr  5572  fliftfund  7322  frfi  9280  fin33i  10451  axdc3lem4  10535  iscatd  17853  isfuncd  18046  isposd  18502  pospropd  18505  imasmnd2  18974  grpinveu  19191  grpid  19192  grpasscan1  19218  imasgrp2  19271  dmdprdd  20221  pgpfac1lem5  20301  imasrng  20405  imasring  20566  islmodd  21147  lmodvsghm  21204  islssd  21216  islmhm2  21319  cmprmidlmcl  21637  mulgghm2  21788  isphld  21966  riinopn  23232  ordtbaslem  23512  subbascn  23578  haust1  23676  isnrm2  23682  isnrm3  23683  lmmo  23704  nllyidm  23814  tx1stc  23975  filin  24179  filtop  24180  isfil2  24181  infil  24188  fgfil  24200  isufil2  24233  ufileu  24244  filufint  24245  flimopn  24300  flimrest  24308  isxmetd  24651  met2ndc  24848  icccmplem2  25149  lmmbr  25585  cfil3i  25596  equivcfil  25626  bcthlem5  25655  volfiniun  25874  dvidlem  26241  ulmdvlem3  26735  ax5seg  29522  axcontlem4  29551  axcont  29560  grporcan  31126  grpoinveu  31127  grpoid  31128  cvxpconn  36094  cvxsconn  36095  mclsax  36421  mclsppslem  36435  r1peuqusdeg1  36495  broutsideof2  36980  nn0prpwlem  37203  fgmin  37251  poimirlem27  38659  poimirlem29  38661  poimirlem31  38663  cntotbnd  38824  heiborlem6  38844  heiborlem10  38848  rngonegmn1l  38969  rngonegmn1r  38970  rngoneglmul  38971  rngonegrmul  38972  crngm23  39030  prnc  39095  pridlc3  39101  dmncan1  39104  lsmsat  40159  eqlkr  40250  llncmp  40673  2at0mat0  40676  llncvrlpln  40709  lplncmp  40713  lplnexllnN  40715  lplncvrlvol  40767  lvolcmp  40768  linepsubN  40903  pmapsub  40919  paddasslem16  40986  pmodlem2  40998  lhp2lt  41152  ltrneq2  41299  cdlemf2  41713  cdlemk34  42061  cdlemn11pre  42361  dihord2pre  42376  onexoegt  44340  clnbgrssedg  49033  clnbgrgrimlem  49125  grimgrtri  49141  idomcanl  49538