MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3exp2 Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 3exp2.1 . . 3 ((𝜑 ∧ (𝜓𝜒𝜃)) → 𝜏)
21ex 415 . 2 (𝜑 → ((𝜓𝜒𝜃) → 𝜏))
323expd 1349 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Colors of variables: wff setvar class
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  5482  predpo  6161  fliftfund  7060  frfi  8757  fin33i  9785  axdc3lem4  9869  relexpaddd  14407  iscatd  16938  isfuncd  17129  isposd  17559  pospropd  17738  imasmnd2  17942  grpinveu  18132  grpid  18133  grpasscan1  18156  imasgrp2  18208  dmdprdd  19115  pgpfac1lem5  19195  imasring  19363  islmodd  19634  lmodvsghm  19689  islssd  19701  islmhm2  19804  psrbaglefi  20146  mulgghm2  20638  isphld  20792  riinopn  21510  ordtbaslem  21790  subbascn  21856  haust1  21954  isnrm2  21960  isnrm3  21961  lmmo  21982  nllyidm  22091  tx1stc  22252  filin  22456  filtop  22457  isfil2  22458  infil  22465  fgfil  22477  isufil2  22510  ufileu  22521  filufint  22522  flimopn  22577  flimrest  22585  isxmetd  22930  met2ndc  23127  icccmplem2  23425  lmmbr  23855  cfil3i  23866  equivcfil  23896  bcthlem5  23925  volfiniun  24142  dvidlem  24507  ulmdvlem3  24984  ax5seg  26718  axcontlem4  26747  axcont  26756  grporcan  28289  grpoinveu  28290  grpoid  28291  cvxpconn  32484  cvxsconn  32485  mclsax  32811  mclsppslem  32825  broutsideof2  33578  nn0prpwlem  33665  fgmin  33713  poimirlem27  34913  poimirlem29  34915  poimirlem31  34917  cntotbnd  35068  heiborlem6  35088  heiborlem10  35092  rngonegmn1l  35213  rngonegmn1r  35214  rngoneglmul  35215  rngonegrmul  35216  crngm23  35274  prnc  35339  pridlc3  35345  dmncan1  35348  lsmsat  36138  eqlkr  36229  llncmp  36652  2at0mat0  36655  llncvrlpln  36688  lplncmp  36692  lplnexllnN  36694  lplncvrlvol  36746  lvolcmp  36747  linepsubN  36882  pmapsub  36898  paddasslem16  36965  pmodlem2  36977  lhp2lt  37131  ltrneq2  37278  cdlemf2  37692  cdlemk34  38040  cdlemn11pre  38340  dihord2pre  38355
  Copyright terms: Public domain W3C validator