Theorem 3exp2 1356

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  3anassrs  1362  pm2.61da3ne  3022  po2nr  5554  fliftfund  7269  frfi  9197  fin33i  10291  axdc3lem4  10375  iscatd  17608  isfuncd  17801  isposd  18257  pospropd  18260  imasmnd2  18711  grpinveu  18916  grpid  18917  grpasscan1  18943  imasgrp2  18997  dmdprdd  19942  pgpfac1lem5  20022  imasrng  20124  imasring  20278  islmodd  20829  lmodvsghm  20886  islssd  20898  islmhm2  21002  mulgghm2  21443  isphld  21621  riinopn  22864  ordtbaslem  23144  subbascn  23210  haust1  23308  isnrm2  23314  isnrm3  23315  lmmo  23336  nllyidm  23445  tx1stc  23606  filin  23810  filtop  23811  isfil2  23812  infil  23819  fgfil  23831  isufil2  23864  ufileu  23875  filufint  23876  flimopn  23931  flimrest  23939  isxmetd  24282  met2ndc  24479  icccmplem2  24780  lmmbr  25226  cfil3i  25237  equivcfil  25267  bcthlem5  25296  volfiniun  25516  dvidlem  25884  ulmdvlem3  26379  ax5seg  29023  axcontlem4  29052  axcont  29061  grporcan  30605  grpoinveu  30606  grpoid  30607  cvxpconn  35455  cvxsconn  35456  mclsax  35782  mclsppslem  35796  r1peuqusdeg1  35856  broutsideof2  36335  nn0prpwlem  36535  fgmin  36583  poimirlem27  37895  poimirlem29  37897  poimirlem31  37899  cntotbnd  38044  heiborlem6  38064  heiborlem10  38068  rngonegmn1l  38189  rngonegmn1r  38190  rngoneglmul  38191  rngonegrmul  38192  crngm23  38250  prnc  38315  pridlc3  38321  dmncan1  38324  lsmsat  39381  eqlkr  39472  llncmp  39895  2at0mat0  39898  llncvrlpln  39931  lplncmp  39935  lplnexllnN  39937  lplncvrlvol  39989  lvolcmp  39990  linepsubN  40125  pmapsub  40141  paddasslem16  40208  pmodlem2  40220  lhp2lt  40374  ltrneq2  40521  cdlemf2  40935  cdlemk34  41283  cdlemn11pre  41583  dihord2pre  41598  onexoegt  43598  clnbgrssedg  48198  clnbgrgrimlem  48290  grimgrtri  48306