Theorem 3exp2 1361

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  3anassrs  1367  pm2.61da3ne  3023  po2nr  5540  fliftfund  7257  frfi  9185  fin33i  10282  axdc3lem4  10366  iscatd  17630  isfuncd  17823  isposd  18279  pospropd  18282  imasmnd2  18733  grpinveu  18941  grpid  18942  grpasscan1  18968  imasgrp2  19022  dmdprdd  19967  pgpfac1lem5  20047  imasrng  20149  imasring  20301  islmodd  20856  lmodvsghm  20913  islssd  20925  islmhm2  21028  mulgghm2  21451  isphld  21629  riinopn  22891  ordtbaslem  23171  subbascn  23237  haust1  23335  isnrm2  23341  isnrm3  23342  lmmo  23363  nllyidm  23472  tx1stc  23633  filin  23837  filtop  23838  isfil2  23839  infil  23846  fgfil  23858  isufil2  23891  ufileu  23902  filufint  23903  flimopn  23958  flimrest  23966  isxmetd  24309  met2ndc  24506  icccmplem2  24807  lmmbr  25243  cfil3i  25254  equivcfil  25284  bcthlem5  25313  volfiniun  25532  dvidlem  25900  ulmdvlem3  26385  ax5seg  29025  axcontlem4  29054  axcont  29063  grporcan  30607  grpoinveu  30608  grpoid  30609  cvxpconn  35470  cvxsconn  35471  mclsax  35797  mclsppslem  35811  r1peuqusdeg1  35871  broutsideof2  36350  nn0prpwlem  36550  fgmin  36598  poimirlem27  38014  poimirlem29  38016  poimirlem31  38018  cntotbnd  38163  heiborlem6  38183  heiborlem10  38187  rngonegmn1l  38308  rngonegmn1r  38309  rngoneglmul  38310  rngonegrmul  38311  crngm23  38369  prnc  38434  pridlc3  38440  dmncan1  38443  lsmsat  39500  eqlkr  39591  llncmp  40014  2at0mat0  40017  llncvrlpln  40050  lplncmp  40054  lplnexllnN  40056  lplncvrlvol  40108  lvolcmp  40109  linepsubN  40244  pmapsub  40260  paddasslem16  40327  pmodlem2  40339  lhp2lt  40493  ltrneq2  40640  cdlemf2  41054  cdlemk34  41402  cdlemn11pre  41702  dihord2pre  41717  onexoegt  43689  clnbgrssedg  48332  clnbgrgrimlem  48424  grimgrtri  48440