Theorem 3exp2 1350

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 399  df-3an 1085

This theorem is referenced by:  3anassrs  1356  pm2.61da3ne  3106  po2nr  5487  predpo  6166  fliftfund  7066  frfi  8763  fin33i  9791  axdc3lem4  9875  relexpaddd  14413  iscatd  16944  isfuncd  17135  isposd  17565  pospropd  17744  imasmnd2  17948  grpinveu  18138  grpid  18139  grpasscan1  18162  imasgrp2  18214  dmdprdd  19121  pgpfac1lem5  19201  imasring  19369  islmodd  19640  lmodvsghm  19695  islssd  19707  islmhm2  19810  psrbaglefi  20152  mulgghm2  20644  isphld  20798  riinopn  21516  ordtbaslem  21796  subbascn  21862  haust1  21960  isnrm2  21966  isnrm3  21967  lmmo  21988  nllyidm  22097  tx1stc  22258  filin  22462  filtop  22463  isfil2  22464  infil  22471  fgfil  22483  isufil2  22516  ufileu  22527  filufint  22528  flimopn  22583  flimrest  22591  isxmetd  22936  met2ndc  23133  icccmplem2  23431  lmmbr  23861  cfil3i  23872  equivcfil  23902  bcthlem5  23931  volfiniun  24148  dvidlem  24513  ulmdvlem3  24990  ax5seg  26724  axcontlem4  26753  axcont  26762  grporcan  28295  grpoinveu  28296  grpoid  28297  cvxpconn  32489  cvxsconn  32490  mclsax  32816  mclsppslem  32830  broutsideof2  33583  nn0prpwlem  33670  fgmin  33718  poimirlem27  34934  poimirlem29  34936  poimirlem31  34938  cntotbnd  35089  heiborlem6  35109  heiborlem10  35113  rngonegmn1l  35234  rngonegmn1r  35235  rngoneglmul  35236  rngonegrmul  35237  crngm23  35295  prnc  35360  pridlc3  35366  dmncan1  35369  lsmsat  36159  eqlkr  36250  llncmp  36673  2at0mat0  36676  llncvrlpln  36709  lplncmp  36713  lplnexllnN  36715  lplncvrlvol  36767  lvolcmp  36768  linepsubN  36903  pmapsub  36919  paddasslem16  36986  pmodlem2  36998  lhp2lt  37152  ltrneq2  37299  cdlemf2  37713  cdlemk34  38061  cdlemn11pre  38361  dihord2pre  38376