Theorem 3exp2 1371

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 401  df-3an 1103

This theorem is referenced by:  3anassrs  1379  pm2.61da3ne  3053  po2nr  5581  fliftfund  7309  frfi  9241  fin33i  10349  axdc3lem4  10433  iscatd  17725  isfuncd  17918  isposd  18374  pospropd  18377  imasmnd2  18828  grpinveu  19037  grpid  19038  grpasscan1  19064  imasgrp2  19117  dmdprdd  20067  pgpfac1lem5  20147  imasrng  20251  imasring  20408  islmodd  20961  lmodvsghm  21018  islssd  21030  islmhm2  21133  mulgghm2  21591  isphld  21769  riinopn  23030  ordtbaslem  23310  subbascn  23376  haust1  23474  isnrm2  23480  isnrm3  23481  lmmo  23502  nllyidm  23611  tx1stc  23772  filin  23976  filtop  23977  isfil2  23978  infil  23985  fgfil  23997  isufil2  24030  ufileu  24041  filufint  24042  flimopn  24097  flimrest  24105  isxmetd  24448  met2ndc  24645  icccmplem2  24946  lmmbr  25382  cfil3i  25393  equivcfil  25423  bcthlem5  25452  volfiniun  25671  dvidlem  26039  ulmdvlem3  26527  ax5seg  29225  axcontlem4  29254  axcont  29263  grporcan  30807  grpoinveu  30808  grpoid  30809  cvxpconn  35629  cvxsconn  35630  mclsax  35956  mclsppslem  35970  r1peuqusdeg1  36030  broutsideof2  36509  nn0prpwlem  36718  fgmin  36766  poimirlem27  38181  poimirlem29  38183  poimirlem31  38185  cntotbnd  38330  heiborlem6  38350  heiborlem10  38354  rngonegmn1l  38475  rngonegmn1r  38476  rngoneglmul  38477  rngonegrmul  38478  crngm23  38536  prnc  38601  pridlc3  38607  dmncan1  38610  lsmsat  39667  eqlkr  39758  llncmp  40181  2at0mat0  40184  llncvrlpln  40217  lplncmp  40221  lplnexllnN  40223  lplncvrlvol  40275  lvolcmp  40276  linepsubN  40411  pmapsub  40427  paddasslem16  40494  pmodlem2  40506  lhp2lt  40660  ltrneq2  40807  cdlemf2  41221  cdlemk34  41569  cdlemn11pre  41869  dihord2pre  41884  onexoegt  43856  clnbgrssedg  48488  clnbgrgrimlem  48580  grimgrtri  48596