MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpisyl Unicode version

Theorem mpisyl 18
Description: A syllogism combined with a modus ponens inference. (Contributed by Alan Sare, 25-Jul-2011.)
Hypotheses
Ref Expression
mpisyl.1
mpisyl.2
mpisyl.3
Assertion
Ref Expression
mpisyl

Proof of Theorem mpisyl
StepHypRef Expression
1 mpisyl.1 . 2
2 mpisyl.2 . . 3
3 mpisyl.3 . . 3
42, 3mpi 17 . 2
51, 4syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4
This theorem is referenced by:  ceqsex  3145  moeq3  3276  reusv1  4652  reusv2lem1  4653  fveqf1o  6205  fliftcnv  6209  fliftfun  6210  undom  7625  pwdom  7689  onomeneq  7727  pwfilem  7834  ordiso  7962  ordtypelem8  7971  wdompwdom  8025  unxpwdom  8036  harwdom  8037  infeq5i  8074  cantnfcl  8107  cantnfclOLD  8137  cardiun  8384  infxpenlem  8412  dfac8b  8433  acnnum  8454  inffien  8465  dfac12lem2  8545  cdadom3  8589  cdainflem  8592  cdainf  8593  infunabs  8608  infcda  8609  infdif  8610  infdif2  8611  infmap2  8619  fictb  8646  cofsmo  8670  fin23lem21  8740  hsmexlem1  8827  iundomg  8937  iunctb  8970  fpwwe2lem9  9037  canthnum  9048  winalim2  9095  rankcf  9176  tskuni  9182  npomex  9395  hashun2  12451  swrd2lsw  12890  2swrd2eqwrdeq  12891  limsupgord  13295  summolem2  13538  zsum  13540  prodmolem2  13742  zprod  13744  isinv  15154  invsym2  15157  invfun  15158  oppcsect2  15169  oppcinv  15170  efgcpbllemb  16773  frgpuplem  16790  gsumval3OLD  16908  gsumval3  16911  bwthOLD  19911  1stcfb  19946  1stcrestlem  19953  2ndcdisj2  19958  txdis1cn  20136  tx1stc  20151  tgphaus  20615  qustgplem  20619  tsmsxp  20657  xmeter  20936  bndth  21458  ovolctb2  21903  ovoliunlem1  21913  i1fd  22088  dvgt0lem2  22404  taylf  22756  efcvx  22844  logccv  23044  loglesqrt  23132  usgraidx2v  24393  frgra3vlem1  25000  numclwlk1lem2f1  25094  stadd3i  27167  strlem6  27175  dmct  27537  cnvct  27538  mptct  27541  mptctf  27544  sibfof  28282  subfaclefac  28620  erdsze2lem1  28647  erdsze2lem2  28648  snmlff  28774  orderseqlem  29332  frrlem5c  29393  heicant  30049  pell1qrgaplem  30809  dnwech  30994  stoweid  31845  dirkercncflem2  31886  fourierdlem36  31925  usgedgvadf1  32415  usgedgvadf1ALT  32418  bnj97  33924  bnj553  33956  bnj966  34002  bnj1442  34105  dvhopellsm  36844
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator