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 412	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏))
3	2	3expd 1352	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 206  df-an 396  df-3an 1088

This theorem is referenced by:  3anassrs  1359  pm2.61da3ne  3030  po2nr  5602  fliftfund  7313  frfi  9294  fin33i  10370  axdc3lem4  10454  iscatd  17624  isfuncd  17822  isposd  18286  pospropd  18290  imasmnd2  18702  grpinveu  18902  grpid  18903  grpasscan1  18929  imasgrp2  18981  dmdprdd  19917  pgpfac1lem5  19997  imasrng  20078  imasring  20225  islmodd  20708  lmodvsghm  20765  islssd  20778  islmhm2  20882  mulgghm2  21336  isphld  21517  psrbaglefiOLD  21796  riinopn  22730  ordtbaslem  23012  subbascn  23078  haust1  23176  isnrm2  23182  isnrm3  23183  lmmo  23204  nllyidm  23313  tx1stc  23474  filin  23678  filtop  23679  isfil2  23680  infil  23687  fgfil  23699  isufil2  23732  ufileu  23743  filufint  23744  flimopn  23799  flimrest  23807  isxmetd  24152  met2ndc  24352  icccmplem2  24659  lmmbr  25106  cfil3i  25117  equivcfil  25147  bcthlem5  25176  volfiniun  25396  dvidlem  25764  ulmdvlem3  26253  ax5seg  28629  axcontlem4  28658  axcont  28667  grporcan  30204  grpoinveu  30205  grpoid  30206  cvxpconn  34697  cvxsconn  34698  mclsax  35024  mclsppslem  35038  broutsideof2  35564  nn0prpwlem  35671  fgmin  35719  poimirlem27  36979  poimirlem29  36981  poimirlem31  36983  cntotbnd  37128  heiborlem6  37148  heiborlem10  37152  rngonegmn1l  37273  rngonegmn1r  37274  rngoneglmul  37275  rngonegrmul  37276  crngm23  37334  prnc  37399  pridlc3  37405  dmncan1  37408  lsmsat  38342  eqlkr  38433  llncmp  38857  2at0mat0  38860  llncvrlpln  38893  lplncmp  38897  lplnexllnN  38899  lplncvrlvol  38951  lvolcmp  38952  linepsubN  39087  pmapsub  39103  paddasslem16  39170  pmodlem2  39182  lhp2lt  39336  ltrneq2  39483  cdlemf2  39897  cdlemk34  40245  cdlemn11pre  40545  dihord2pre  40560  onexoegt  42456