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  1707  tbwlem2  1708  re1luk3  1714  merco1lem17  1735  re1tbw1  1747  spimew  1975  snssg  4742  relcnvtrg  6216  relresfld  6226  onfr  6354  foimacnv  6798  fvi  6914  isoini2  7280  ovidig  7493  f1oexbi  7861  frxp  8054  smores2  8296  tfrlem5  8322  en2sn  8981  en2snOLD  8982  en2prd  8988  mapdom1  9082  php2OLD  9163  snnen2oOLD  9167  frfi  9228  fodomfi  9265  ixpfi2  9290  hartogs  9476  wemapsolem  9482  card2on  9486  unwdomg  9516  ttrclss  9652  r1pwss  9716  tz9.12lem3  9721  uniwf  9751  rankval3b  9758  djuun  9858  tskwe  9882  carddomi2  9902  cardsdomelir  9905  infxpenlem  9945  inffien  9995  alephord  10007  alephdom  10013  iunfictbso  10046  dfac8  10067  dfacacn  10073  dfac13  10074  dfac12lem2  10076  infmap2  10150  ackbij1b  10171  ackbij2  10175  fictb  10177  cfslb  10198  fin67  10327  fin1a2lem10  10341  fin1a2lem11  10342  dcomex  10379  ttukeylem1  10441  ttukeylem7  10447  ondomon  10495  konigthlem  10500  alephadd  10509  alephexp1  10511  alephreg  10514  pwcfsdom  10515  fpwwe2lem12  10574  gchaleph  10603  gchaleph2  10604  winainflem  10625  inttsk  10706  inar1  10707  inatsk  10710  grudomon  10749  nqerid  10865  nqpr  10946  zmin  12861  uzrdgsuci  13857  isfinite4  14254  pfxccatin12lem3  14612  limsupval2  15354  sumz  15599  fsumsers  15605  isumclim  15634  ntrivcvgfvn0  15776  ntrivcvgtail  15777  zprodn0  15814  iprodclim  15873  alzdvds  16194  bitsfzolem  16306  phicl2  16632  phibnd  16635  pclem  16702  strle1  17022  fnpr2ob  17432  psss  18461  symg2bas  19165  dprdss  19799  2ndcdisj  22791  dis2ndc  22795  hausmapdom  22835  ptcnplem  22956  fbun  23175  metrest  23864  opnreen  24178  ivthle  24804  ivthle2  24805  ovolfiniun  24849  volfiniun  24895  uniiccdif  24926  uniioovol  24927  uniioombllem4  24934  dyadmbl  24948  vitali  24961  mbflimsup  25014  cpnres  25285  dvcj  25298  dvef  25328  dvne0  25359  lhop2  25363  itgparts  25395  itgsubstlem  25396  ply1divex  25485  fta1blem  25517  dgrlem  25574  pige3ALT  25860  xrlimcnp  26302  ftalem3  26408  lgsdchr  26687  2lgslem1  26726  addsqn2reu  26773  2sqreultblem  26780  2sqreunnltblem  26783  dchrvmasumlem2  26830  pntlem3  26941  tgisline  27455  axcontlem2  27800  upgrex  27929  umgrnloop2  27983  usgriedgleord  28062  uspgredgleord  28066  nbedgusgr  28206  nb3grprlem2  28215  rusgrnumwrdl2  28420  wlkp1lem2  28508  wwlksnexthasheq  28734  wlksnwwlknvbij  28739  2pthon3v  28774  umgr2wlk  28780  rusgrnumwlkg  28808  umgrclwwlkge2  28821  clwwlkvbij  28943  0pthonv  28959  1pthon2v  28983  numclwwlkqhash  29205  chscllem4  30468  adjeq  30763  hmopidmchi  30979  xreceu  31661  tocyccntz  31876  archirngz  31908  archiabllem1b  31911  locfinreflem  32290  measvuni  32682  elmbfmvol2  32736  omsmeas  32792  sibfof  32809  eulerpartlemgvv  32845  ballotlemfc0  32961  ballotlemfcc  32962  iccllysconn  33713  cvmliftphtlem  33780  satfv1  33826  sat1el2xp  33842  opnrebl2  34760  re1ax2lem  34826  re1ax2  34827  bj-orim2  34986  bj-peircecurry  34988  lindsdom  36039  poimir  36078  volsupnfl  36090  areacirc  36138  totbndbnd  36215  islsati  37423  hdmap14lem2a  40297  rabdiophlem1  41062  pellexlem5  41094  ttac  41298  aomclem4  41322  hbtlem5  41393  idomodle  41461  idomsubgmo  41463  nnoeomeqom  41584  omabs2  41603  rp-isfinite5  41731  iscard4  41747  mnuunid  42499  vk15.4j  42752  ax6e2nd  42782  trsspwALT2  43043  sspwtrALT  43046  sstrALT2  43059  dvmptconst  44088  dvmptidg  44090  fperdvper  44092  dvmulcncf  44098  dvdivcncf  44100  fourierdlem20  44300  fouriercn  44405  ndmaovcl  45367  fundcmpsurinjpreimafv  45532  fmtnofac2  45693  prminf2  45712  isomuspgrlem2  45957  irinitoringc  46299  pgrpgt2nabl  46374  line2x  46772  prstchom2ALT  47031  spcdvw  47056  aacllem  47180
  Copyright terms: Public domain W3C validator