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

Theorem mpsyl 68
Description: Modus ponens combined with a syllogism inference. (Contributed by Alan Sare, 20-Apr-2011.)
Hypotheses
Ref Expression
mpsyl.1 𝜑
mpsyl.2 (𝜓𝜒)
mpsyl.3 (𝜑 → (𝜒𝜃))
Assertion
Ref Expression
mpsyl (𝜓𝜃)

Proof of Theorem mpsyl
StepHypRef Expression
1 mpsyl.1 . . 3 𝜑
21a1i 11 . 2 (𝜓𝜑)
3 mpsyl.2 . 2 (𝜓𝜒)
4 mpsyl.3 . 2 (𝜑 → (𝜒𝜃))
52, 3, 4sylc 65 1 (𝜓𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  tbwlem1  1670  tbwlem2  1671  re1luk3  1677  merco1lem17  1698  re1tbw1  1710  relcnvtr  5693  relresfld  5700  onfr  5801  foimacnv  6192  fvi  6294  isoini2  6629  ovidig  6820  f1oexbi  7158  frxp  7332  smores2  7496  tfrlem5  7521  mapdom1  8166  php2  8186  snnen2o  8190  frfi  8246  fodomfi  8280  ixpfi2  8305  hartogs  8490  wemapsolem  8496  card2on  8500  unwdomg  8530  r1pwss  8685  tz9.12lem3  8690  uniwf  8720  rankval3b  8727  tskwe  8814  carddomi2  8834  cardsdomelir  8837  infxpenlem  8874  inffien  8924  alephord  8936  alephdom  8942  iunfictbso  8975  dfac8  8995  dfacacn  9001  dfac13  9002  dfac12lem2  9004  infmap2  9078  ackbij1b  9099  ackbij2  9103  fictb  9105  cfslb  9126  fin67  9255  fin1a2lem10  9269  fin1a2lem11  9270  dcomex  9307  ttukeylem1  9369  ttukeylem7  9375  ondomon  9423  konigthlem  9428  alephadd  9437  alephexp1  9439  alephreg  9442  pwcfsdom  9443  fpwwe2lem13  9502  gchaleph  9531  gchaleph2  9532  winainflem  9553  inttsk  9634  inar1  9635  inatsk  9638  grudomon  9677  nqerid  9793  nqpr  9874  zmin  11822  uzrdgsuci  12799  isfinite4  13191  swrdccatin12lem3  13536  limsupval2  14255  caucvgb  14454  sumz  14497  fsumsers  14503  isumclim  14532  isumnn0nn  14618  climcndslem1  14625  climcndslem2  14626  ntrivcvgfvn0  14675  ntrivcvgtail  14676  zprodn0  14713  iprodclim  14773  alzdvds  15089  bitsfzolem  15203  phicl2  15520  phibnd  15523  pclem  15590  strle1  16020  psss  17261  symg2bas  17864  dprdss  18474  2ndcdisj  21307  dis2ndc  21311  hausmapdom  21351  ptcnplem  21472  fbun  21691  metrest  22376  opnreen  22681  bndth  22804  cmetcaulem  23132  ivthle  23271  ivthle2  23272  ovolfiniun  23315  volfiniun  23361  uniiccdif  23392  uniioovol  23393  uniioombllem4  23400  dyadmbl  23414  vitali  23427  mbfdm  23440  mbflimsup  23478  itg2monolem2  23563  itg2monolem3  23564  itg2mono  23565  cpnres  23745  dvcj  23758  dvef  23788  dvne0  23819  lhop2  23823  itgparts  23855  itgsubstlem  23856  ply1divex  23941  fta1blem  23973  dgrlem  24030  pige3  24314  xrlimcnp  24740  lgambdd  24808  ftalem3  24846  lgsdchr  25125  2lgslem1  25164  dchrvmasumlem2  25232  pntlem3  25343  tgisline  25567  axcontlem2  25890  upgrex  26032  umgrnloop2  26086  usgriedgleord  26165  uspgredgleord  26169  nbedgusgr  26318  nb3grprlem2  26327  rusgrnumwrdl2  26538  wlkp1lem2  26627  wlknwwlksnbij2  26846  wlkwwlkbij2  26853  wwlksnexthasheq  26866  wlksnwwlknvbij  26871  2pthon3v  26908  umgr2wlk  26914  rusgrnumwlkg  26944  umgrclwwlkge2  26957  clwwlkbij  27015  clwwlkvbij  27088  clwwlkvbijOLD  27089  0pthonv  27107  1pthon2v  27131  numclwlk1lem2  27350  numclwwlk1  27351  numclwwlkqhash  27355  chscllem4  28627  adjeq  28922  hmopidmchi  29138  xreceu  29758  archirngz  29871  archiabllem1b  29874  locfinreflem  30035  measvuni  30405  elmbfmvol2  30457  omsmeas  30513  sibfof  30530  eulerpartlemgvv  30566  ballotlemfc0  30682  ballotlemfcc  30683  iccllysconn  31358  cvmliftphtlem  31425  opnrebl2  32441  re1ax2lem  32507  re1ax2  32508  bj-orim2  32666  bj-currypeirce  32669  bj-peircecurry  32670  lindsdom  33533  poimir  33572  volsupnfl  33584  areacirc  33635  totbndbnd  33718  islsati  34599  hdmap14lem2a  37476  rabdiophlem1  37682  pellexlem5  37714  ttac  37920  aomclem4  37944  hbtlem5  38015  idomodle  38091  idomsubgmo  38093  rp-isfinite5  38180  vk15.4j  39051  ax6e2nd  39091  eel0001  39262  trsspwALT2  39363  sspwtrALT  39366  sstrALT2  39384  dvmptconst  40447  dvmptidg  40449  fperdvper  40451  dvmulcncf  40458  dvdivcncf  40460  fourierdlem20  40662  fouriercn  40767  ndmaovcl  41604  fmtnofac2  41806  prminf2  41825  irinitoringc  42394  pgrpgt2nabl  42472  spcdvw  42751  aacllem  42875
  Copyright terms: Public domain W3C validator