Theorem 3exp2 1352

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 1351	1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  3anassrs  1358  pm2.61da3ne  3033  po2nr  5508  fliftfund  7164  frfi  8989  fin33i  10056  axdc3lem4  10140  iscatd  17299  isfuncd  17496  isposd  17956  pospropd  17960  imasmnd2  18337  grpinveu  18529  grpid  18530  grpasscan1  18553  imasgrp2  18605  dmdprdd  19517  pgpfac1lem5  19597  imasring  19773  islmodd  20044  lmodvsghm  20099  islssd  20112  islmhm2  20215  mulgghm2  20610  isphld  20771  psrbaglefiOLD  21046  riinopn  21965  ordtbaslem  22247  subbascn  22313  haust1  22411  isnrm2  22417  isnrm3  22418  lmmo  22439  nllyidm  22548  tx1stc  22709  filin  22913  filtop  22914  isfil2  22915  infil  22922  fgfil  22934  isufil2  22967  ufileu  22978  filufint  22979  flimopn  23034  flimrest  23042  isxmetd  23387  met2ndc  23585  icccmplem2  23892  lmmbr  24327  cfil3i  24338  equivcfil  24368  bcthlem5  24397  volfiniun  24616  dvidlem  24984  ulmdvlem3  25466  ax5seg  27209  axcontlem4  27238  axcont  27247  grporcan  28781  grpoinveu  28782  grpoid  28783  cvxpconn  33104  cvxsconn  33105  mclsax  33431  mclsppslem  33445  broutsideof2  34351  nn0prpwlem  34438  fgmin  34486  poimirlem27  35731  poimirlem29  35733  poimirlem31  35735  cntotbnd  35881  heiborlem6  35901  heiborlem10  35905  rngonegmn1l  36026  rngonegmn1r  36027  rngoneglmul  36028  rngonegrmul  36029  crngm23  36087  prnc  36152  pridlc3  36158  dmncan1  36161  lsmsat  36949  eqlkr  37040  llncmp  37463  2at0mat0  37466  llncvrlpln  37499  lplncmp  37503  lplnexllnN  37505  lplncvrlvol  37557  lvolcmp  37558  linepsubN  37693  pmapsub  37709  paddasslem16  37776  pmodlem2  37788  lhp2lt  37942  ltrneq2  38089  cdlemf2  38503  cdlemk34  38851  cdlemn11pre  39151  dihord2pre  39166