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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  3anassrs  1361  pm2.61da3ne  3032  po2nr  5603  fliftfund  7310  frfi  9288  fin33i  10364  axdc3lem4  10448  iscatd  17617  isfuncd  17815  isposd  18276  pospropd  18280  imasmnd2  18662  grpinveu  18859  grpid  18860  grpasscan1  18886  imasgrp2  18938  dmdprdd  19869  pgpfac1lem5  19949  imasring  20143  islmodd  20477  lmodvsghm  20533  islssd  20546  islmhm2  20649  mulgghm2  21046  isphld  21207  psrbaglefiOLD  21486  riinopn  22410  ordtbaslem  22692  subbascn  22758  haust1  22856  isnrm2  22862  isnrm3  22863  lmmo  22884  nllyidm  22993  tx1stc  23154  filin  23358  filtop  23359  isfil2  23360  infil  23367  fgfil  23379  isufil2  23412  ufileu  23423  filufint  23424  flimopn  23479  flimrest  23487  isxmetd  23832  met2ndc  24032  icccmplem2  24339  lmmbr  24775  cfil3i  24786  equivcfil  24816  bcthlem5  24845  volfiniun  25064  dvidlem  25432  ulmdvlem3  25914  ax5seg  28196  axcontlem4  28225  axcont  28234  grporcan  29771  grpoinveu  29772  grpoid  29773  cvxpconn  34233  cvxsconn  34234  mclsax  34560  mclsppslem  34574  broutsideof2  35094  nn0prpwlem  35207  fgmin  35255  poimirlem27  36515  poimirlem29  36517  poimirlem31  36519  cntotbnd  36664  heiborlem6  36684  heiborlem10  36688  rngonegmn1l  36809  rngonegmn1r  36810  rngoneglmul  36811  rngonegrmul  36812  crngm23  36870  prnc  36935  pridlc3  36941  dmncan1  36944  lsmsat  37878  eqlkr  37969  llncmp  38393  2at0mat0  38396  llncvrlpln  38429  lplncmp  38433  lplnexllnN  38435  lplncvrlvol  38487  lvolcmp  38488  linepsubN  38623  pmapsub  38639  paddasslem16  38706  pmodlem2  38718  lhp2lt  38872  ltrneq2  39019  cdlemf2  39433  cdlemk34  39781  cdlemn11pre  40081  dihord2pre  40096  onexoegt  41993  imasrng  46678