Theorem 3exp2 1353

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 1352	1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  3anassrs  1359  pm2.61da3ne  3035  po2nr  5518  fliftfund  7193  frfi  9068  fin33i  10134  axdc3lem4  10218  iscatd  17391  isfuncd  17589  isposd  18050  pospropd  18054  imasmnd2  18431  grpinveu  18623  grpid  18624  grpasscan1  18647  imasgrp2  18699  dmdprdd  19611  pgpfac1lem5  19691  imasring  19867  islmodd  20138  lmodvsghm  20193  islssd  20206  islmhm2  20309  mulgghm2  20707  isphld  20868  psrbaglefiOLD  21145  riinopn  22066  ordtbaslem  22348  subbascn  22414  haust1  22512  isnrm2  22518  isnrm3  22519  lmmo  22540  nllyidm  22649  tx1stc  22810  filin  23014  filtop  23015  isfil2  23016  infil  23023  fgfil  23035  isufil2  23068  ufileu  23079  filufint  23080  flimopn  23135  flimrest  23143  isxmetd  23488  met2ndc  23688  icccmplem2  23995  lmmbr  24431  cfil3i  24442  equivcfil  24472  bcthlem5  24501  volfiniun  24720  dvidlem  25088  ulmdvlem3  25570  ax5seg  27315  axcontlem4  27344  axcont  27353  grporcan  28889  grpoinveu  28890  grpoid  28891  cvxpconn  33213  cvxsconn  33214  mclsax  33540  mclsppslem  33554  broutsideof2  34433  nn0prpwlem  34520  fgmin  34568  poimirlem27  35813  poimirlem29  35815  poimirlem31  35817  cntotbnd  35963  heiborlem6  35983  heiborlem10  35987  rngonegmn1l  36108  rngonegmn1r  36109  rngoneglmul  36110  rngonegrmul  36111  crngm23  36169  prnc  36234  pridlc3  36240  dmncan1  36243  lsmsat  37029  eqlkr  37120  llncmp  37543  2at0mat0  37546  llncvrlpln  37579  lplncmp  37583  lplnexllnN  37585  lplncvrlvol  37637  lvolcmp  37638  linepsubN  37773  pmapsub  37789  paddasslem16  37856  pmodlem2  37868  lhp2lt  38022  ltrneq2  38169  cdlemf2  38583  cdlemk34  38931  cdlemn11pre  39231  dihord2pre  39246