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  3021  po2nr  5546  fliftfund  7259  frfi  9185  fin33i  10279  axdc3lem4  10363  iscatd  17596  isfuncd  17789  isposd  18245  pospropd  18248  imasmnd2  18699  grpinveu  18904  grpid  18905  grpasscan1  18931  imasgrp2  18985  dmdprdd  19930  pgpfac1lem5  20010  imasrng  20112  imasring  20266  islmodd  20817  lmodvsghm  20874  islssd  20886  islmhm2  20990  mulgghm2  21431  isphld  21609  riinopn  22852  ordtbaslem  23132  subbascn  23198  haust1  23296  isnrm2  23302  isnrm3  23303  lmmo  23324  nllyidm  23433  tx1stc  23594  filin  23798  filtop  23799  isfil2  23800  infil  23807  fgfil  23819  isufil2  23852  ufileu  23863  filufint  23864  flimopn  23919  flimrest  23927  isxmetd  24270  met2ndc  24467  icccmplem2  24768  lmmbr  25214  cfil3i  25225  equivcfil  25255  bcthlem5  25284  volfiniun  25504  dvidlem  25872  ulmdvlem3  26367  ax5seg  29011  axcontlem4  29040  axcont  29049  grporcan  30593  grpoinveu  30594  grpoid  30595  cvxpconn  35436  cvxsconn  35437  mclsax  35763  mclsppslem  35777  r1peuqusdeg1  35837  broutsideof2  36316  nn0prpwlem  36516  fgmin  36564  poimirlem27  37848  poimirlem29  37850  poimirlem31  37852  cntotbnd  37997  heiborlem6  38017  heiborlem10  38021  rngonegmn1l  38142  rngonegmn1r  38143  rngoneglmul  38144  rngonegrmul  38145  crngm23  38203  prnc  38268  pridlc3  38274  dmncan1  38277  lsmsat  39268  eqlkr  39359  llncmp  39782  2at0mat0  39785  llncvrlpln  39818  lplncmp  39822  lplnexllnN  39824  lplncvrlvol  39876  lvolcmp  39877  linepsubN  40012  pmapsub  40028  paddasslem16  40095  pmodlem2  40107  lhp2lt  40261  ltrneq2  40408  cdlemf2  40822  cdlemk34  41170  cdlemn11pre  41470  dihord2pre  41485  onexoegt  43486  clnbgrssedg  48087  clnbgrgrimlem  48179  grimgrtri  48195