Theorem 3exp2 1467

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

Syntax hints:   → wi 4   ∧ wa 386   ∧ w3a 1111

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 199  df-an 387  df-3an 1113

This theorem is referenced by:  3anassrs  1473  pm2.61da3ne  3088  po2nr  5278  predpo  5942  fliftfund  6823  frfi  8480  fin33i  9513  axdc3lem4  9597  relexpaddd  14178  iscatd  16693  isfuncd  16884  isposd  17315  pospropd  17494  imasmnd2  17687  grpinveu  17817  grpid  17818  grpasscan1  17839  imasgrp2  17891  dmdprdd  18759  pgpfac1lem5  18839  imasring  18980  islmodd  19232  lmodvsghm  19287  islssd  19299  islmhm2  19404  psrbaglefi  19740  mulgghm2  20212  isphld  20368  riinopn  21090  ordtbaslem  21370  subbascn  21436  haust1  21534  isnrm2  21540  isnrm3  21541  lmmo  21562  nllyidm  21670  tx1stc  21831  filin  22035  filtop  22036  isfil2  22037  infil  22044  fgfil  22056  isufil2  22089  ufileu  22100  filufint  22101  flimopn  22156  flimrest  22164  isxmetd  22508  met2ndc  22705  icccmplem2  23003  lmmbr  23433  cfil3i  23444  equivcfil  23474  bcthlem5  23503  volfiniun  23720  dvidlem  24085  ulmdvlem3  24562  ax5seg  26244  axcontlem4  26273  axcont  26282  grporcan  27924  grpoinveu  27925  grpoid  27926  cvxpconn  31766  cvxsconn  31767  mclsax  32008  mclsppslem  32022  broutsideof2  32763  nn0prpwlem  32850  fgmin  32898  poimirlem27  33975  poimirlem29  33977  poimirlem31  33979  cntotbnd  34132  heiborlem6  34152  heiborlem10  34156  rngonegmn1l  34277  rngonegmn1r  34278  rngoneglmul  34279  rngonegrmul  34280  crngm23  34338  prnc  34403  pridlc3  34409  dmncan1  34412  lsmsat  35078  eqlkr  35169  llncmp  35592  2at0mat0  35595  llncvrlpln  35628  lplncmp  35632  lplnexllnN  35634  lplncvrlvol  35686  lvolcmp  35687  linepsubN  35822  pmapsub  35838  paddasslem16  35905  pmodlem2  35917  lhp2lt  36071  ltrneq2  36218  cdlemf2  36632  cdlemk34  36980  cdlemn11pre  37280  dihord2pre  37295