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  1699  tbwlem2  1700  re1luk3  1706  merco1lem17  1727  re1tbw1  1739  spimew  1967  relcnvtrg  6116  relresfld  6124  onfr  6227  foimacnv  6628  fvi  6736  isoini2  7087  ovidig  7285  f1oexbi  7624  frxp  7814  smores2  7985  tfrlem5  8010  mapdom1  8674  php2  8694  snnen2o  8699  frfi  8755  fodomfi  8789  ixpfi2  8814  hartogs  9000  wemapsolem  9006  card2on  9010  unwdomg  9040  r1pwss  9205  tz9.12lem3  9210  uniwf  9240  rankval3b  9247  djuun  9347  tskwe  9371  carddomi2  9391  cardsdomelir  9394  infxpenlem  9431  inffien  9481  alephord  9493  alephdom  9499  iunfictbso  9532  dfac8  9553  dfacacn  9559  dfac13  9560  dfac12lem2  9562  infmap2  9632  ackbij1b  9653  ackbij2  9657  fictb  9659  cfslb  9680  fin67  9809  fin1a2lem10  9823  fin1a2lem11  9824  dcomex  9861  ttukeylem1  9923  ttukeylem7  9929  ondomon  9977  konigthlem  9982  alephadd  9991  alephexp1  9993  alephreg  9996  pwcfsdom  9997  fpwwe2lem13  10056  gchaleph  10085  gchaleph2  10086  winainflem  10107  inttsk  10188  inar1  10189  inatsk  10192  grudomon  10231  nqerid  10347  nqpr  10428  zmin  12336  uzrdgsuci  13321  isfinite4  13716  pfxccatin12lem3  14087  limsupval2  14830  sumz  15071  fsumsers  15077  isumclim  15104  ntrivcvgfvn0  15247  ntrivcvgtail  15248  zprodn0  15285  iprodclim  15344  alzdvds  15662  bitsfzolem  15775  phicl2  16097  phibnd  16100  pclem  16167  strle1  16584  fnpr2ob  16823  psss  17816  symg2bas  18448  dprdss  19073  2ndcdisj  21980  dis2ndc  21984  hausmapdom  22024  ptcnplem  22145  fbun  22364  metrest  23049  opnreen  23354  ivthle  23972  ivthle2  23973  ovolfiniun  24017  volfiniun  24063  uniiccdif  24094  uniioovol  24095  uniioombllem4  24102  dyadmbl  24116  vitali  24129  mbflimsup  24182  cpnres  24449  dvcj  24462  dvef  24492  dvne0  24523  lhop2  24527  itgparts  24559  itgsubstlem  24560  ply1divex  24645  fta1blem  24677  dgrlem  24734  pige3ALT  25020  xrlimcnp  25460  ftalem3  25566  lgsdchr  25845  2lgslem1  25884  addsqn2reu  25931  2sqreultblem  25938  2sqreunnltblem  25941  dchrvmasumlem2  25988  pntlem3  26099  tgisline  26327  axcontlem2  26666  upgrex  26792  umgrnloop2  26846  usgriedgleord  26925  uspgredgleord  26929  nbedgusgr  27069  nb3grprlem2  27078  rusgrnumwrdl2  27283  wlkp1lem2  27371  wwlksnexthasheq  27596  wlksnwwlknvbij  27602  2pthon3v  27637  umgr2wlk  27643  rusgrnumwlkg  27671  umgrclwwlkge2  27684  clwwlkvbij  27807  0pthonv  27823  1pthon2v  27847  numclwwlkqhash  28069  chscllem4  29332  adjeq  29627  hmopidmchi  29843  xreceu  30513  tocyccntz  30701  archirngz  30733  archiabllem1b  30736  locfinreflem  30991  measvuni  31360  elmbfmvol2  31412  omsmeas  31468  sibfof  31485  eulerpartlemgvv  31521  ballotlemfc0  31637  ballotlemfcc  31638  iccllysconn  32382  cvmliftphtlem  32449  satfv1  32495  sat1el2xp  32511  opnrebl2  33554  re1ax2lem  33620  re1ax2  33621  bj-orim2  33776  bj-peircecurry  33778  lindsdom  34754  poimir  34793  volsupnfl  34805  areacirc  34855  totbndbnd  34936  islsati  35998  hdmap14lem2a  38871  rabdiophlem1  39260  pellexlem5  39292  ttac  39495  aomclem4  39519  hbtlem5  39590  idomodle  39658  idomsubgmo  39660  rp-isfinite5  39745  iscard4  39762  mnuunid  40475  vk15.4j  40724  ax6e2nd  40754  trsspwALT2  41015  sspwtrALT  41018  sstrALT2  41031  dvmptconst  42061  dvmptidg  42063  fperdvper  42065  dvmulcncf  42072  dvdivcncf  42074  fourierdlem20  42275  fouriercn  42380  ndmaovcl  43265  fmtnofac2  43560  prminf2  43579  isomuspgrlem2  43827  irinitoringc  44169  pgrpgt2nabl  44243  line2x  44570  spcdvw  44611  aacllem  44731
  Copyright terms: Public domain W3C validator