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

Theorem exp32 409
Description: An exportation inference. (Contributed by NM, 26-Apr-1994.)
Hypothesis
Ref Expression
exp32.1 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
Assertion
Ref Expression
exp32 (𝜑 → (𝜓 → (𝜒𝜃)))

Proof of Theorem exp32
StepHypRef Expression
1 exp32.1 . . 3 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
21ex 399 . 2 (𝜑 → ((𝜓𝜒) → 𝜃))
32expd 402 1 (𝜑 → (𝜓 → (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 198  df-an 385
This theorem is referenced by:  exp44  426  exp45  427  expr  446  anassrs  455  an13s  633  3impb  1136  wereu  5304  f0rn0  6302  funfvima3  6717  isomin  6808  isoini  6809  ovg  7026  elovmpt3rab1  7120  onint  7222  peano5  7316  tfrlem11  7717  tz7.48lem  7769  oalimcl  7874  oaass  7875  resixpfo  8180  fundmen  8263  php3  8382  ssfi  8416  fodomfi  8475  marypha1lem  8575  card2inf  8696  ixpiunwdom  8732  cantnflt  8813  cnfcom  8841  dfac3  9224  dfac5lem5  9230  dfac5  9231  cfcoflem  9376  fin1a2s  9518  zorn2lem4  9603  zorn2lem7  9606  fpwwe2lem12  9745  wunfi  9825  grur1a  9923  addcanpi  10003  mulcanpi  10004  distrlem1pr  10129  ltaddpr  10138  ltexprlem1  10140  ltexprlem6  10145  ltexprlem7  10146  prodgt0  11150  mulgt1  11164  uzwo  11966  xmulasslem  12329  xlemul1a  12332  faclbnd  13293  swrdccatin12lem2a  13705  swrdccat3  13712  swrdccat  13713  cshwidxmod  13769  s3iunsndisj  13928  dvdsaddre2b  15248  divgcdcoprm0  15593  cncongr2  15596  infpnlem1  15827  isacs4lem  17369  gsmsymgrfixlem1  18044  gsmsymgrfix  18045  dmdprdsplit2lem  18642  pgpfac1  18677  pgpfac  18681  lssssr  19155  lssssrOLD  19156  islmhm2  19241  lspdisj  19328  cygznlem2a  20119  lindfmm  20372  scmataddcl  20529  scmatsubcl  20530  scmatmulcl  20531  cayhamlem3  20901  cayleyhamilton1  20906  neindisj  21131  cnpnei  21278  t0dist  21339  ordthauslem  21397  uncmp  21416  fiuncmp  21417  iunconnlem  21440  fbasrn  21897  rnelfmlem  21965  rnelfm  21966  fmfnfmlem2  21968  fmfnfmlem4  21970  fclscf  22038  alexsubALTlem3  22062  alexsubALTlem4  22063  alexsubALT  22064  reconn  22840  fsumcn  22882  ovolfiniun  23478  dyadmax  23575  dyadmbllem  23576  dvmptfsum  23948  dvlip2  23968  dvivthlem1  23981  dvcnvrelem1  23990  ply1divex  24106  fta1g  24137  plydivex  24262  fta1  24273  mulcxp  24641  zabsle1  25231  lgsquad2lem2  25320  2lgsoddprm  25351  pntlem3  25508  brbtwn  25989  brcgr  25990  brbtwn2  25995  axeuclid  26053  finsumvtxdg2size  26670  uhgrwkspthlem2  26874  crctcshwlkn0  26938  wwlksnred  27025  wwlksnextinj  27032  wspthsnwspthsnonOLD  27052  umgr2wlk  27085  elwwlks2  27104  clwlkclwwlklem2a  27137  clwlkclwwlkf1lem3  27145  wwlksext2clwwlkOLD  27204  eupth2lems  27407  numclwwlk2lem1lem  27514  numclwwlk2lem1lemOLD  27515  frgrregord013  27579  grpoidinvlem3  27685  shorth  28479  pjhthmo  28486  pjpjpre  28603  elspansn5  28758  lnopmi  29184  adjlnop  29270  leopmul2i  29319  stlesi  29425  ssmd2  29496  dmdsl3  29499  mdexchi  29519  cvexchlem  29552  atcv1  29564  atcvatlem  29569  atabsi  29585  mdsymlem2  29588  mdsymlem5  29591  sumdmdii  29599  sumdmdlem  29602  sumdmdlem2  29603  dya2iocnrect  30665  bnj571  31296  pconnconn  31533  iccllysconn  31552  trpredmintr  32048  poseq  32071  nodenselem8  32159  nocvxmin  32212  cgrextend  32433  btwnexch2  32448  colineardim1  32486  lineext  32501  btwnconn1lem13  32524  btwnconn1lem14  32525  seglecgr12im  32535  outsideofeq  32555  outsideofeu  32556  nn0prpwlem  32635  neibastop2lem  32673  tailfb  32690  nndivsub  32770  ee7.2aOLD  32774  poimirlem31  33750  heicant  33754  filbcmb  33844  prdsbnd2  33902  heibor  33928  rngoisocnv  34088  ax12eq  34717  ax12el  34718  pmodlem2  35624  cdleme22b  36119  cdleme32d  36222  cdleme32f  36224  trlord  36347  cdlemj2  36600  cdlemk38  36693  cdlemk19x  36721  dihord2pre  37003  mzpcompact2lem  37813  pellfundex  37949  acongsym  38041  pwssplit4  38157  pwslnm  38162  relexpmulg  38499  stoweidlem17  40710  iccpartigtl  41931  pfxccat3  41998  fmtnofac2lem  42052  2pwp1prmfmtno  42076  lighneallem4  42099  bgoldbtbndlem2  42266  bgoldbtbndlem3  42267  bgoldbtbnd  42269  lmod0rng  42433  2zrngamgm  42504
  Copyright terms: Public domain W3C validator