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 1086

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 1088

This theorem is referenced by:  3anassrs  1361  pm2.61da3ne  3018  po2nr  5543  fliftfund  7256  frfi  9180  fin33i  10271  axdc3lem4  10355  iscatd  17587  isfuncd  17780  isposd  18236  pospropd  18239  imasmnd2  18690  grpinveu  18895  grpid  18896  grpasscan1  18922  imasgrp2  18976  dmdprdd  19921  pgpfac1lem5  20001  imasrng  20103  imasring  20257  islmodd  20808  lmodvsghm  20865  islssd  20877  islmhm2  20981  mulgghm2  21422  isphld  21600  riinopn  22843  ordtbaslem  23123  subbascn  23189  haust1  23287  isnrm2  23293  isnrm3  23294  lmmo  23315  nllyidm  23424  tx1stc  23585  filin  23789  filtop  23790  isfil2  23791  infil  23798  fgfil  23810  isufil2  23843  ufileu  23854  filufint  23855  flimopn  23910  flimrest  23918  isxmetd  24261  met2ndc  24458  icccmplem2  24759  lmmbr  25205  cfil3i  25216  equivcfil  25246  bcthlem5  25275  volfiniun  25495  dvidlem  25863  ulmdvlem3  26358  ax5seg  28937  axcontlem4  28966  axcont  28975  grporcan  30519  grpoinveu  30520  grpoid  30521  cvxpconn  35358  cvxsconn  35359  mclsax  35685  mclsppslem  35699  r1peuqusdeg1  35759  broutsideof2  36238  nn0prpwlem  36438  fgmin  36486  poimirlem27  37760  poimirlem29  37762  poimirlem31  37764  cntotbnd  37909  heiborlem6  37929  heiborlem10  37933  rngonegmn1l  38054  rngonegmn1r  38055  rngoneglmul  38056  rngonegrmul  38057  crngm23  38115  prnc  38180  pridlc3  38186  dmncan1  38189  lsmsat  39180  eqlkr  39271  llncmp  39694  2at0mat0  39697  llncvrlpln  39730  lplncmp  39734  lplnexllnN  39736  lplncvrlvol  39788  lvolcmp  39789  linepsubN  39924  pmapsub  39940  paddasslem16  40007  pmodlem2  40019  lhp2lt  40173  ltrneq2  40320  cdlemf2  40734  cdlemk34  41082  cdlemn11pre  41382  dihord2pre  41397  onexoegt  43401  clnbgrssedg  48003  clnbgrgrimlem  48095  grimgrtri  48111