Theorem 3exp2 1355

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 1088

This theorem is referenced by:  3anassrs  1361  pm2.61da3ne  3015  po2nr  5563  fliftfund  7291  frfi  9239  fin33i  10329  axdc3lem4  10413  iscatd  17641  isfuncd  17834  isposd  18290  pospropd  18293  imasmnd2  18708  grpinveu  18913  grpid  18914  grpasscan1  18940  imasgrp2  18994  dmdprdd  19938  pgpfac1lem5  20018  imasrng  20093  imasring  20246  islmodd  20779  lmodvsghm  20836  islssd  20848  islmhm2  20952  mulgghm2  21393  isphld  21570  riinopn  22802  ordtbaslem  23082  subbascn  23148  haust1  23246  isnrm2  23252  isnrm3  23253  lmmo  23274  nllyidm  23383  tx1stc  23544  filin  23748  filtop  23749  isfil2  23750  infil  23757  fgfil  23769  isufil2  23802  ufileu  23813  filufint  23814  flimopn  23869  flimrest  23877  isxmetd  24221  met2ndc  24418  icccmplem2  24719  lmmbr  25165  cfil3i  25176  equivcfil  25206  bcthlem5  25235  volfiniun  25455  dvidlem  25823  ulmdvlem3  26318  ax5seg  28872  axcontlem4  28901  axcont  28910  grporcan  30454  grpoinveu  30455  grpoid  30456  cvxpconn  35236  cvxsconn  35237  mclsax  35563  mclsppslem  35577  r1peuqusdeg1  35637  broutsideof2  36117  nn0prpwlem  36317  fgmin  36365  poimirlem27  37648  poimirlem29  37650  poimirlem31  37652  cntotbnd  37797  heiborlem6  37817  heiborlem10  37821  rngonegmn1l  37942  rngonegmn1r  37943  rngoneglmul  37944  rngonegrmul  37945  crngm23  38003  prnc  38068  pridlc3  38074  dmncan1  38077  lsmsat  39008  eqlkr  39099  llncmp  39523  2at0mat0  39526  llncvrlpln  39559  lplncmp  39563  lplnexllnN  39565  lplncvrlvol  39617  lvolcmp  39618  linepsubN  39753  pmapsub  39769  paddasslem16  39836  pmodlem2  39848  lhp2lt  40002  ltrneq2  40149  cdlemf2  40563  cdlemk34  40911  cdlemn11pre  41211  dihord2pre  41226  onexoegt  43240  clnbgrssedg  47845  clnbgrgrimlem  47937  grimgrtri  47952