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

Theorem exp32 628
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 448 . 2 (𝜑 → ((𝜓𝜒) → 𝜃))
32expd 450 1 (𝜑 → (𝜓 → (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  exp44  638  exp45  639  expr  640  anassrs  677  an13s  840  3impb  1251  reusv2lem2OLD  4787  wereu  5020  f0rn0  5984  funfvima3  6373  isomin  6461  isoini  6462  ovg  6671  elovmpt3rab1  6764  onint  6860  peano5  6954  tfrlem11  7344  tz7.48lem  7396  oalimcl  7500  oaass  7501  resixpfo  7805  fundmen  7889  php3  8004  ssfi  8038  fodomfi  8097  marypha1lem  8195  card2inf  8316  ixpiunwdom  8352  cantnflt  8425  cnfcom  8453  dfac3  8800  dfac5lem5  8806  dfac5  8807  cfcoflem  8950  fin1a2s  9092  zorn2lem4  9177  zorn2lem7  9180  fpwwe2lem12  9315  wunfi  9395  grur1a  9493  addcanpi  9573  mulcanpi  9574  distrlem1pr  9699  ltaddpr  9708  ltexprlem1  9710  ltexprlem6  9715  ltexprlem7  9716  prodgt0  10713  mulgt1  10727  uzwo  11579  xmulasslem  11940  xlemul1a  11943  faclbnd  12890  swrdccatin12lem2a  13278  swrdccat3  13285  swrdccat  13286  cshwidxmod  13342  s3iunsndisj  13497  dvdsaddre2b  14809  divgcdcoprm0  15159  cncongr2  15162  infpnlem1  15394  isacs4lem  16933  gsmsymgrfixlem1  17612  gsmsymgrfix  17613  dmdprdsplit2lem  18209  pgpfac1  18244  pgpfac  18248  lssssr  18716  islmhm2  18801  lspdisj  18888  cygznlem2a  19676  lindfmm  19923  scmataddcl  20079  scmatsubcl  20080  scmatmulcl  20081  cayhamlem3  20449  cayleyhamilton1  20454  neindisj  20669  cnpnei  20816  t0dist  20877  ordthauslem  20935  uncmp  20954  fiuncmp  20955  iunconlem  20978  fbasrn  21436  rnelfmlem  21504  rnelfm  21505  fmfnfmlem2  21507  fmfnfmlem4  21509  fclscf  21577  alexsubALTlem3  21601  alexsubALTlem4  21602  alexsubALT  21603  reconn  22367  fsumcn  22408  ovolfiniun  22989  dyadmax  23085  dyadmbllem  23086  dvmptfsum  23455  dvlip2  23475  dvivthlem1  23488  dvcnvrelem1  23497  ply1divex  23613  fta1g  23644  plydivex  23769  fta1  23780  mulcxp  24144  zabsle1  24734  lgsquad2lem2  24823  2lgsoddprm  24854  pntlem3  25011  brbtwn  25493  brcgr  25494  brbtwn2  25499  axeuclid  25557  wwlknred  26013  wwlkextinj  26020  clwlkisclwwlklem2a  26075  wwlkext2clwwlk  26093  eupath2  26269  clwwlkextfrlem1  26365  frgraregord013  26407  grpoidinvlem3  26506  shorth  27340  pjhthmo  27347  pjpjpre  27464  elspansn5  27619  lnopmi  28045  adjlnop  28131  leopmul2i  28180  stlesi  28286  ssmd2  28357  dmdsl3  28360  mdexchi  28380  cvexchlem  28413  atcv1  28425  atcvatlem  28430  atabsi  28446  mdsymlem2  28449  mdsymlem5  28452  sumdmdii  28460  sumdmdlem  28463  sumdmdlem2  28464  dya2iocnrect  29472  bnj571  30032  pconcon  30269  iccllyscon  30288  trpredmintr  30777  poseq  30796  nodenselem8  30889  nocvxmin  30892  cgrextend  31087  btwnexch2  31102  colineardim1  31140  lineext  31155  btwnconn1lem13  31178  btwnconn1lem14  31179  seglecgr12im  31189  outsideofeq  31209  outsideofeu  31210  nn0prpwlem  31289  neibastop2lem  31327  tailfb  31344  nndivsub  31428  ee7.2aOLD  31432  poimirlem31  32409  heicant  32413  filbcmb  32504  prdsbnd2  32563  heibor  32589  rngoisocnv  32749  ax12eq  33043  ax12el  33044  pmodlem2  33950  cdleme22b  34446  cdleme32d  34549  cdleme32f  34551  trlord  34674  cdlemj2  34927  cdlemk38  35020  cdlemk19x  35048  dihord2pre  35331  mzpcompact2lem  36131  pellfundex  36267  acongsym  36360  pwssplit4  36476  pwslnm  36481  relexpmulg  36820  stoweidlem17  38710  iccpartigtl  39762  fmtnofac2lem  39819  2pwp1prmfmtno  39843  lighneallem4  39866  bgoldbtbndlem2  40023  bgoldbtbndlem3  40024  bgoldbtbnd  40026  pfxccat3  40090  uhgr1wlkspthlem2  40958  crctcsh1wlkn0  41022  wwlksnred  41096  wwlksnextinj  41103  wspthsnwspthsnon  41120  umgr2wlk  41154  elwwlks2  41168  clwlkclwwlklem2a  41205  wwlksext2clwwlk  41229  eupth2lems  41404  frgrwopreglem2  41480  av-clwwlkextfrlem1  41507  av-frgraregord013  41547  lmod0rng  41656  2zrngamgm  41727
  Copyright terms: Public domain W3C validator