Theorem 3exp2 1351

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  3anassrs  1357  pm2.61da3ne  3076  po2nr  5451  predpo  6134  fliftfund  7045  frfi  8747  fin33i  9780  axdc3lem4  9864  iscatd  16936  isfuncd  17127  isposd  17557  pospropd  17736  imasmnd2  17940  grpinveu  18130  grpid  18131  grpasscan1  18154  imasgrp2  18206  dmdprdd  19114  pgpfac1lem5  19194  imasring  19365  islmodd  19633  lmodvsghm  19688  islssd  19700  islmhm2  19803  mulgghm2  20190  isphld  20343  psrbaglefi  20610  riinopn  21513  ordtbaslem  21793  subbascn  21859  haust1  21957  isnrm2  21963  isnrm3  21964  lmmo  21985  nllyidm  22094  tx1stc  22255  filin  22459  filtop  22460  isfil2  22461  infil  22468  fgfil  22480  isufil2  22513  ufileu  22524  filufint  22525  flimopn  22580  flimrest  22588  isxmetd  22933  met2ndc  23130  icccmplem2  23428  lmmbr  23862  cfil3i  23873  equivcfil  23903  bcthlem5  23932  volfiniun  24151  dvidlem  24518  ulmdvlem3  24997  ax5seg  26732  axcontlem4  26761  axcont  26770  grporcan  28301  grpoinveu  28302  grpoid  28303  cvxpconn  32602  cvxsconn  32603  mclsax  32929  mclsppslem  32943  broutsideof2  33696  nn0prpwlem  33783  fgmin  33831  poimirlem27  35084  poimirlem29  35086  poimirlem31  35088  cntotbnd  35234  heiborlem6  35254  heiborlem10  35258  rngonegmn1l  35379  rngonegmn1r  35380  rngoneglmul  35381  rngonegrmul  35382  crngm23  35440  prnc  35505  pridlc3  35511  dmncan1  35514  lsmsat  36304  eqlkr  36395  llncmp  36818  2at0mat0  36821  llncvrlpln  36854  lplncmp  36858  lplnexllnN  36860  lplncvrlvol  36912  lvolcmp  36913  linepsubN  37048  pmapsub  37064  paddasslem16  37131  pmodlem2  37143  lhp2lt  37297  ltrneq2  37444  cdlemf2  37858  cdlemk34  38206  cdlemn11pre  38506  dihord2pre  38521