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  1382  pm2.61da3ne  3048  po2nr  5580  fliftfund  7352  frfi  9314  fin33i  10486  axdc3lem4  10570  iscatd  17897  isfuncd  18090  isposd  18546  pospropd  18549  imasmnd2  19018  grpinveu  19235  grpid  19236  grpasscan1  19262  imasgrp2  19315  dmdprdd  20266  pgpfac1lem5  20346  imasrng  20450  imasring  20611  islmodd  21192  lmodvsghm  21249  islssd  21261  islmhm2  21364  cmprmidlmcl  21682  mulgghm2  21837  isphld  22015  riinopn  23281  ordtbaslem  23561  subbascn  23627  haust1  23725  isnrm2  23731  isnrm3  23732  lmmo  23753  nllyidm  23863  tx1stc  24024  filin  24228  filtop  24229  isfil2  24230  infil  24237  fgfil  24249  isufil2  24282  ufileu  24293  filufint  24294  flimopn  24349  flimrest  24357  isxmetd  24700  met2ndc  24897  icccmplem2  25198  lmmbr  25634  cfil3i  25645  equivcfil  25675  bcthlem5  25704  volfiniun  25923  dvidlem  26290  ulmdvlem3  26786  ax5seg  29573  axcontlem4  29602  axcont  29611  grporcan  31177  grpoinveu  31178  grpoid  31179  cvxpconn  36215  cvxsconn  36216  mclsax  36542  mclsppslem  36556  r1peuqusdeg1  36616  broutsideof2  37102  nn0prpwlem  37325  fgmin  37373  poimirlem27  38833  poimirlem29  38835  poimirlem31  38837  cntotbnd  38996  heiborlem6  39016  heiborlem10  39020  rngonegmn1l  39141  rngonegmn1r  39142  rngoneglmul  39143  rngonegrmul  39144  crngm23  39202  prnc  39267  pridlc3  39273  dmncan1  39276  lsmsat  40331  eqlkr  40422  llncmp  40845  2at0mat0  40848  llncvrlpln  40881  lplncmp  40885  lplnexllnN  40887  lplncvrlvol  40939  lvolcmp  40940  linepsubN  41075  pmapsub  41091  paddasslem16  41158  pmodlem2  41170  lhp2lt  41324  ltrneq2  41471  cdlemf2  41885  cdlemk34  42233  cdlemn11pre  42533  dihord2pre  42548  onexoegt  44507  clnbgrssedg  49212  clnbgrgrimlem  49304  grimgrtri  49320  idomcanl  49775