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  3049  po2nr  5585  fliftfund  7317  frfi  9248  fin33i  10364  axdc3lem4  10448  iscatd  17746  isfuncd  17939  isposd  18395  pospropd  18398  imasmnd2  18855  grpinveu  19064  grpid  19065  grpasscan1  19091  imasgrp2  19144  dmdprdd  20094  pgpfac1lem5  20174  imasrng  20278  imasring  20437  islmodd  21016  lmodvsghm  21073  islssd  21085  islmhm2  21188  cmprmidlmcl  21504  mulgghm2  21655  isphld  21833  riinopn  23094  ordtbaslem  23374  subbascn  23440  haust1  23538  isnrm2  23544  isnrm3  23545  lmmo  23566  nllyidm  23675  tx1stc  23836  filin  24040  filtop  24041  isfil2  24042  infil  24049  fgfil  24061  isufil2  24094  ufileu  24105  filufint  24106  flimopn  24161  flimrest  24169  isxmetd  24512  met2ndc  24709  icccmplem2  25010  lmmbr  25446  cfil3i  25457  equivcfil  25487  bcthlem5  25516  volfiniun  25735  dvidlem  26103  ulmdvlem3  26594  ax5seg  29317  axcontlem4  29346  axcont  29355  grporcan  30899  grpoinveu  30900  grpoid  30901  cvxpconn  35747  cvxsconn  35748  mclsax  36074  mclsppslem  36088  r1peuqusdeg1  36148  broutsideof2  36627  nn0prpwlem  36866  fgmin  36914  poimirlem27  38331  poimirlem29  38333  poimirlem31  38335  cntotbnd  38480  heiborlem6  38500  heiborlem10  38504  rngonegmn1l  38625  rngonegmn1r  38626  rngoneglmul  38627  rngonegrmul  38628  crngm23  38686  prnc  38751  pridlc3  38757  dmncan1  38760  lsmsat  39815  eqlkr  39906  llncmp  40329  2at0mat0  40332  llncvrlpln  40365  lplncmp  40369  lplnexllnN  40371  lplncvrlvol  40423  lvolcmp  40424  linepsubN  40559  pmapsub  40575  paddasslem16  40642  pmodlem2  40654  lhp2lt  40808  ltrneq2  40955  cdlemf2  41369  cdlemk34  41717  cdlemn11pre  42017  dihord2pre  42032  onexoegt  44004  clnbgrssedg  48639  clnbgrgrimlem  48731  grimgrtri  48747  idomcanl  49145