Theorem 3exp2 1367

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  3anassrs  1373  pm2.61da3ne  3045  po2nr  5565  fliftfund  7292  frfi  9223  fin33i  10320  axdc3lem4  10404  iscatd  17696  isfuncd  17889  isposd  18345  pospropd  18348  imasmnd2  18799  grpinveu  19007  grpid  19008  grpasscan1  19034  imasgrp2  19088  dmdprdd  20032  pgpfac1lem5  20112  imasrng  20214  imasring  20366  islmodd  20921  lmodvsghm  20978  islssd  20990  islmhm2  21093  mulgghm2  21516  isphld  21694  riinopn  22956  ordtbaslem  23236  subbascn  23302  haust1  23400  isnrm2  23406  isnrm3  23407  lmmo  23428  nllyidm  23537  tx1stc  23698  filin  23902  filtop  23903  isfil2  23904  infil  23911  fgfil  23923  isufil2  23956  ufileu  23967  filufint  23968  flimopn  24023  flimrest  24031  isxmetd  24374  met2ndc  24571  icccmplem2  24872  lmmbr  25308  cfil3i  25319  equivcfil  25349  bcthlem5  25378  volfiniun  25597  dvidlem  25965  ulmdvlem3  26453  ax5seg  29096  axcontlem4  29125  axcont  29134  grporcan  30678  grpoinveu  30679  grpoid  30680  cvxpconn  35553  cvxsconn  35554  mclsax  35880  mclsppslem  35894  r1peuqusdeg1  35954  broutsideof2  36433  nn0prpwlem  36643  fgmin  36691  poimirlem27  38107  poimirlem29  38109  poimirlem31  38111  cntotbnd  38256  heiborlem6  38276  heiborlem10  38280  rngonegmn1l  38401  rngonegmn1r  38402  rngoneglmul  38403  rngonegrmul  38404  crngm23  38462  prnc  38527  pridlc3  38533  dmncan1  38536  lsmsat  39593  eqlkr  39684  llncmp  40107  2at0mat0  40110  llncvrlpln  40143  lplncmp  40147  lplnexllnN  40149  lplncvrlvol  40201  lvolcmp  40202  linepsubN  40337  pmapsub  40353  paddasslem16  40420  pmodlem2  40432  lhp2lt  40586  ltrneq2  40733  cdlemf2  41147  cdlemk34  41495  cdlemn11pre  41795  dihord2pre  41810  onexoegt  43782  clnbgrssedg  48424  clnbgrgrimlem  48516  grimgrtri  48532