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  5545  fliftfund  7254  frfi  9190  fin33i  10282  axdc3lem4  10366  iscatd  17598  isfuncd  17791  isposd  18247  pospropd  18250  imasmnd2  18667  grpinveu  18872  grpid  18873  grpasscan1  18899  imasgrp2  18953  dmdprdd  19899  pgpfac1lem5  19979  imasrng  20081  imasring  20234  islmodd  20788  lmodvsghm  20845  islssd  20857  islmhm2  20961  mulgghm2  21402  isphld  21580  riinopn  22812  ordtbaslem  23092  subbascn  23158  haust1  23256  isnrm2  23262  isnrm3  23263  lmmo  23284  nllyidm  23393  tx1stc  23554  filin  23758  filtop  23759  isfil2  23760  infil  23767  fgfil  23779  isufil2  23812  ufileu  23823  filufint  23824  flimopn  23879  flimrest  23887  isxmetd  24231  met2ndc  24428  icccmplem2  24729  lmmbr  25175  cfil3i  25186  equivcfil  25216  bcthlem5  25245  volfiniun  25465  dvidlem  25833  ulmdvlem3  26328  ax5seg  28902  axcontlem4  28931  axcont  28940  grporcan  30481  grpoinveu  30482  grpoid  30483  cvxpconn  35234  cvxsconn  35235  mclsax  35561  mclsppslem  35575  r1peuqusdeg1  35635  broutsideof2  36115  nn0prpwlem  36315  fgmin  36363  poimirlem27  37646  poimirlem29  37648  poimirlem31  37650  cntotbnd  37795  heiborlem6  37815  heiborlem10  37819  rngonegmn1l  37940  rngonegmn1r  37941  rngoneglmul  37942  rngonegrmul  37943  crngm23  38001  prnc  38066  pridlc3  38072  dmncan1  38075  lsmsat  39006  eqlkr  39097  llncmp  39521  2at0mat0  39524  llncvrlpln  39557  lplncmp  39561  lplnexllnN  39563  lplncvrlvol  39615  lvolcmp  39616  linepsubN  39751  pmapsub  39767  paddasslem16  39834  pmodlem2  39846  lhp2lt  40000  ltrneq2  40147  cdlemf2  40561  cdlemk34  40909  cdlemn11pre  41209  dihord2pre  41224  onexoegt  43237  clnbgrssedg  47845  clnbgrgrimlem  47937  grimgrtri  47953