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  3014  po2nr  5553  fliftfund  7270  frfi  9208  fin33i  10298  axdc3lem4  10382  iscatd  17610  isfuncd  17803  isposd  18259  pospropd  18262  imasmnd2  18677  grpinveu  18882  grpid  18883  grpasscan1  18909  imasgrp2  18963  dmdprdd  19907  pgpfac1lem5  19987  imasrng  20062  imasring  20215  islmodd  20748  lmodvsghm  20805  islssd  20817  islmhm2  20921  mulgghm2  21362  isphld  21539  riinopn  22771  ordtbaslem  23051  subbascn  23117  haust1  23215  isnrm2  23221  isnrm3  23222  lmmo  23243  nllyidm  23352  tx1stc  23513  filin  23717  filtop  23718  isfil2  23719  infil  23726  fgfil  23738  isufil2  23771  ufileu  23782  filufint  23783  flimopn  23838  flimrest  23846  isxmetd  24190  met2ndc  24387  icccmplem2  24688  lmmbr  25134  cfil3i  25145  equivcfil  25175  bcthlem5  25204  volfiniun  25424  dvidlem  25792  ulmdvlem3  26287  ax5seg  28841  axcontlem4  28870  axcont  28879  grporcan  30420  grpoinveu  30421  grpoid  30422  cvxpconn  35202  cvxsconn  35203  mclsax  35529  mclsppslem  35543  r1peuqusdeg1  35603  broutsideof2  36083  nn0prpwlem  36283  fgmin  36331  poimirlem27  37614  poimirlem29  37616  poimirlem31  37618  cntotbnd  37763  heiborlem6  37783  heiborlem10  37787  rngonegmn1l  37908  rngonegmn1r  37909  rngoneglmul  37910  rngonegrmul  37911  crngm23  37969  prnc  38034  pridlc3  38040  dmncan1  38043  lsmsat  38974  eqlkr  39065  llncmp  39489  2at0mat0  39492  llncvrlpln  39525  lplncmp  39529  lplnexllnN  39531  lplncvrlvol  39583  lvolcmp  39584  linepsubN  39719  pmapsub  39735  paddasslem16  39802  pmodlem2  39814  lhp2lt  39968  ltrneq2  40115  cdlemf2  40529  cdlemk34  40877  cdlemn11pre  41177  dihord2pre  41192  onexoegt  43206  clnbgrssedg  47814  clnbgrgrimlem  47906  grimgrtri  47921