Theorem 3exp2 1362

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1093

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 209  df-an 398  df-3an 1095

This theorem is referenced by:  3anassrs  1368  pm2.61da3ne  3025  po2nr  5543  fliftfund  7261  frfi  9189  fin33i  10286  axdc3lem4  10370  iscatd  17634  isfuncd  17827  isposd  18283  pospropd  18286  imasmnd2  18737  grpinveu  18945  grpid  18946  grpasscan1  18972  imasgrp2  19026  dmdprdd  19971  pgpfac1lem5  20051  imasrng  20153  imasring  20305  islmodd  20860  lmodvsghm  20917  islssd  20929  islmhm2  21032  mulgghm2  21455  isphld  21633  riinopn  22895  ordtbaslem  23175  subbascn  23241  haust1  23339  isnrm2  23345  isnrm3  23346  lmmo  23367  nllyidm  23476  tx1stc  23637  filin  23841  filtop  23842  isfil2  23843  infil  23850  fgfil  23862  isufil2  23895  ufileu  23906  filufint  23907  flimopn  23962  flimrest  23970  isxmetd  24313  met2ndc  24510  icccmplem2  24811  lmmbr  25247  cfil3i  25258  equivcfil  25288  bcthlem5  25317  volfiniun  25536  dvidlem  25904  ulmdvlem3  26389  ax5seg  29029  axcontlem4  29058  axcont  29067  grporcan  30611  grpoinveu  30612  grpoid  30613  cvxpconn  35485  cvxsconn  35486  mclsax  35812  mclsppslem  35826  r1peuqusdeg1  35886  broutsideof2  36365  nn0prpwlem  36565  fgmin  36613  poimirlem27  38029  poimirlem29  38031  poimirlem31  38033  cntotbnd  38178  heiborlem6  38198  heiborlem10  38202  rngonegmn1l  38323  rngonegmn1r  38324  rngoneglmul  38325  rngonegrmul  38326  crngm23  38384  prnc  38449  pridlc3  38455  dmncan1  38458  lsmsat  39515  eqlkr  39606  llncmp  40029  2at0mat0  40032  llncvrlpln  40065  lplncmp  40069  lplnexllnN  40071  lplncvrlvol  40123  lvolcmp  40124  linepsubN  40259  pmapsub  40275  paddasslem16  40342  pmodlem2  40354  lhp2lt  40508  ltrneq2  40655  cdlemf2  41069  cdlemk34  41417  cdlemn11pre  41717  dihord2pre  41732  onexoegt  43704  clnbgrssedg  48346  clnbgrgrimlem  48438  grimgrtri  48454