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  5577  fliftfund  7314  frfi  9255  fin33i  10371  axdc3lem4  10455  iscatd  17761  isfuncd  17954  isposd  18410  pospropd  18413  imasmnd2  18881  grpinveu  19098  grpid  19099  grpasscan1  19125  imasgrp2  19178  dmdprdd  20128  pgpfac1lem5  20208  imasrng  20312  imasring  20471  islmodd  21050  lmodvsghm  21107  islssd  21119  islmhm2  21222  cmprmidlmcl  21538  mulgghm2  21689  isphld  21867  riinopn  23133  ordtbaslem  23413  subbascn  23479  haust1  23577  isnrm2  23583  isnrm3  23584  lmmo  23605  nllyidm  23715  tx1stc  23876  filin  24080  filtop  24081  isfil2  24082  infil  24089  fgfil  24101  isufil2  24134  ufileu  24145  filufint  24146  flimopn  24201  flimrest  24209  isxmetd  24552  met2ndc  24749  icccmplem2  25050  lmmbr  25486  cfil3i  25497  equivcfil  25527  bcthlem5  25556  volfiniun  25775  dvidlem  26142  ulmdvlem3  26638  ax5seg  29395  axcontlem4  29424  axcont  29433  grporcan  30999  grpoinveu  31000  grpoid  31001  cvxpconn  35821  cvxsconn  35822  mclsax  36148  mclsppslem  36162  r1peuqusdeg1  36222  broutsideof2  36702  nn0prpwlem  36941  fgmin  36989  poimirlem27  38396  poimirlem29  38398  poimirlem31  38400  cntotbnd  38546  heiborlem6  38566  heiborlem10  38570  rngonegmn1l  38691  rngonegmn1r  38692  rngoneglmul  38693  rngonegrmul  38694  crngm23  38752  prnc  38817  pridlc3  38823  dmncan1  38826  lsmsat  39881  eqlkr  39972  llncmp  40395  2at0mat0  40398  llncvrlpln  40431  lplncmp  40435  lplnexllnN  40437  lplncvrlvol  40489  lvolcmp  40490  linepsubN  40625  pmapsub  40641  paddasslem16  40708  pmodlem2  40720  lhp2lt  40874  ltrneq2  41021  cdlemf2  41435  cdlemk34  41783  cdlemn11pre  42083  dihord2pre  42098  onexoegt  44085  clnbgrssedg  48757  clnbgrgrimlem  48849  grimgrtri  48865  idomcanl  49262