Theorem 3exp2 1354

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1087

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 1089

This theorem is referenced by:  3anassrs  1360  pm2.61da3ne  3031  po2nr  5601  fliftfund  7306  frfi  9284  fin33i  10360  axdc3lem4  10444  iscatd  17613  isfuncd  17811  isposd  18272  pospropd  18276  imasmnd2  18658  grpinveu  18855  grpid  18856  grpasscan1  18882  imasgrp2  18934  dmdprdd  19863  pgpfac1lem5  19943  imasring  20136  islmodd  20469  lmodvsghm  20525  islssd  20538  islmhm2  20641  mulgghm2  21037  isphld  21198  psrbaglefiOLD  21477  riinopn  22401  ordtbaslem  22683  subbascn  22749  haust1  22847  isnrm2  22853  isnrm3  22854  lmmo  22875  nllyidm  22984  tx1stc  23145  filin  23349  filtop  23350  isfil2  23351  infil  23358  fgfil  23370  isufil2  23403  ufileu  23414  filufint  23415  flimopn  23470  flimrest  23478  isxmetd  23823  met2ndc  24023  icccmplem2  24330  lmmbr  24766  cfil3i  24777  equivcfil  24807  bcthlem5  24836  volfiniun  25055  dvidlem  25423  ulmdvlem3  25905  ax5seg  28185  axcontlem4  28214  axcont  28223  grporcan  29758  grpoinveu  29759  grpoid  29760  cvxpconn  34221  cvxsconn  34222  mclsax  34548  mclsppslem  34562  broutsideof2  35082  nn0prpwlem  35195  fgmin  35243  poimirlem27  36503  poimirlem29  36505  poimirlem31  36507  cntotbnd  36652  heiborlem6  36672  heiborlem10  36676  rngonegmn1l  36797  rngonegmn1r  36798  rngoneglmul  36799  rngonegrmul  36800  crngm23  36858  prnc  36923  pridlc3  36929  dmncan1  36932  lsmsat  37866  eqlkr  37957  llncmp  38381  2at0mat0  38384  llncvrlpln  38417  lplncmp  38421  lplnexllnN  38423  lplncvrlvol  38475  lvolcmp  38476  linepsubN  38611  pmapsub  38627  paddasslem16  38694  pmodlem2  38706  lhp2lt  38860  ltrneq2  39007  cdlemf2  39421  cdlemk34  39769  cdlemn11pre  40069  dihord2pre  40084  onexoegt  41978  imasrng  46664