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

Theorem syl5bi 217
Description: A mixed syllogism inference from a nested implication and a biconditional. Useful for substituting an embedded antecedent with a definition. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl5bi.1  |-  ( ph  <->  ps )
syl5bi.2  |-  ( ch 
->  ( ps  ->  th )
)
Assertion
Ref Expression
syl5bi  |-  ( ch 
->  ( ph  ->  th )
)

Proof of Theorem syl5bi
StepHypRef Expression
1 syl5bi.1 . . 3  |-  ( ph  <->  ps )
21biimpi 194 . 2  |-  ( ph  ->  ps )
3 syl5bi.2 . 2  |-  ( ch 
->  ( ps  ->  th )
)
42, 3syl5 32 1  |-  ( ch 
->  ( ph  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
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 185
This theorem is referenced by:  3imtr4g  270  ancomsd  451  3jao  1272  ax12indn  2245  2euex  2349  necon3bd  2635  necon2ad  2649  necon1ad  2668  pm2.61dne  2678  eqneqall  2695  spcimgft  3037  rspc  3056  rspcimdv  3063  euind  3135  reuind  3151  sbciegft  3205  rspsbc  3264  pwpw0  4009  sssn  4019  eqsn  4022  prel12  4037  prnebg  4042  pwsnALT  4074  intss1  4131  intmin  4136  uniintsn  4153  iinss  4209  disji2  4267  disjiun  4270  disjxiun  4277  disjss3  4279  trel3  4381  trin  4383  trintss  4389  eusvnfb  4476  reusv3  4488  copsexg  4564  copsexgOLD  4565  po3nr  4642  fri  4669  wefrc  4701  wereu2  4704  onfr  4745  ord0eln0  4760  onmindif  4795  frsn  4896  ssrelrel  4927  relop  4977  iss  5142  restidsing  5150  poirr2  5210  xpcan  5262  xpcan2  5263  sossfld  5273  funopg  5438  funssres  5446  funun  5448  fv3  5691  fvmptt  5777  iinpreima  5821  suppssOLD  5824  dff3  5844  dff4  5845  fmptsng  5887  fnprb  5923  fnprOLD  5924  fvclss  5946  isomin  6015  isofrlem  6018  weniso  6032  oprabid  6104  ssorduni  6386  onmindif2  6412  limuni3  6452  tfis2f  6455  tfinds  6459  tfinds2  6463  tfinds3  6464  funcnvuni  6519  f1oweALT  6550  f1o2ndf1  6669  poxp  6673  soxp  6674  fnse  6678  suppimacnv  6690  mpt2xopynvov0g  6720  reldmtpos  6742  rntpos  6747  onfununi  6788  smoiun  6808  tfrlem1  6821  tfr3  6844  frsucmptn  6880  tz7.49  6886  oaordi  6973  oawordeulem  6981  omeulem1  7009  oeordi  7014  oelimcl  7027  nnaordi  7045  nneob  7079  omsmolem  7080  erdisj  7136  qsss  7149  uniinqs  7168  th3qlem1  7194  map0g  7240  resixpfo  7289  ixpsnf1o  7291  xpdom3  7397  mapdom3  7471  phplem4  7481  php3  7485  unxpdomlem3  7507  ssfi  7521  findcard2  7540  findcard3  7543  frfi  7545  isfiniteg  7560  xpfi  7571  fiint  7576  finsschain  7606  dffi2  7661  marypha1lem  7671  marypha2  7677  supmo  7690  suplub2  7699  ordiso2  7717  ordtypelem7  7726  ordtypelem8  7727  brwdom2  7776  unxpwdom2  7791  ixpiunwdom  7794  elirrv  7800  suc11reg  7813  noinfep  7853  cantnfle  7867  cantnflem1  7885  cantnf  7889  cantnfleOLD  7897  cantnflem1OLD  7908  cantnfOLD  7911  trcl  7936  epfrs  7939  rankpwi  8018  rankunb  8045  rankuni2b  8048  rankxplim3  8076  cplem1  8084  karden  8090  carddom2  8135  fseqenlem2  8183  ac10ct  8192  acni2  8204  acndom  8209  infpwfien  8220  alephordi  8232  alephord  8233  iunfictbso  8272  aceq3lem  8278  dfac5  8286  dfac2  8288  dfac12lem3  8302  dfac12r  8303  cdainflem  8348  cdainf  8349  cfub  8406  cfeq0  8413  coflim  8418  cfslb2n  8425  cofsmo  8426  coftr  8430  infpssr  8465  fin23lem7  8473  fin23lem11  8474  fin23lem21  8496  isf32lem2  8511  isf34lem4  8534  isfin1-2  8542  isfin1-3  8543  fin1a2lem9  8565  fin1a2lem11  8567  fin1a2lem12  8568  fin1a2lem13  8569  domtriomlem  8599  axdc3lem2  8608  axcclem  8614  ac6c4  8638  zorn2lem4  8656  zorn2lem5  8657  zorn2lem7  8659  ttukeylem5  8670  ttukeyg  8674  brdom6disj  8687  fnrndomg  8690  iunfo  8691  iundom2g  8692  ficard  8717  konigthlem  8720  alephval2  8724  pwcfsdom  8735  fpwwe2lem9  8793  fpwwe2lem11  8795  fpwwe2lem12  8796  fpwwe2lem13  8797  pwfseqlem3  8815  gchpwdom  8825  winalim2  8851  gchina  8854  wunex2  8893  tskr1om2  8923  tskxpss  8927  inar1  8930  tskuni  8938  gruun  8961  grudomon  8972  grur1  8975  ltmpi  9061  ltexprlem2  9194  ltexprlem6  9198  reclem2pr  9205  reclem3pr  9206  reclem4pr  9207  suplem1pr  9209  mulgt0sr  9260  supsrlem  9266  axrrecex  9318  axpre-sup  9324  ltlen  9464  mulge0b  10187  supmul1  10283  supmullem1  10284  supmullem2  10285  supmul  10286  infmrcl  10297  cju  10306  nnsub  10348  0mnnnnn0  10600  un0addcl  10601  un0mulcl  10602  nn0sub  10618  nn0n0n1ge2b  10632  peano5uzi  10718  uzletr  10857  negn0  10929  zsupss  10932  qbtwnre  11157  xrsupexmnf  11255  xrinfmexpnf  11256  xrsupsslem  11257  xrinfmsslem  11258  xrub  11262  supxrun  11266  xrinfm0  11287  ixxdisj  11303  icodisj  11397  difreicc  11404  uzsubsubfz  11458  elfzmlbp  11478  fzofzim  11577  elfznelfzo  11614  injresinj  11623  flval3  11647  modirr  11753  seqf1o  11831  expcl2lem  11861  expnegz  11882  expaddz  11892  expmulz  11894  facwordi  12049  faclbnd4lem4  12056  bccl  12082  hashnfinnn0  12114  hashgt12el  12157  hashgt12el2  12158  hash2pwpr  12166  hashfun  12183  hashbclem  12189  hashbc  12190  hashfacen  12191  hashf1lem1  12192  hashf1  12194  brfi1uzind  12203  wrdind  12355  wrd2ind  12356  swrdccatin1  12358  swrdccatin2  12362  swrdccat3  12367  swrdccat3blem  12370  cshw1  12440  sqrlem1  12716  sqrlem6  12721  rexanre  12818  cau3lem  12826  2clim  13034  summo  13178  fsum2dlem  13221  fsumiun  13267  rpnnen2  13491  odd2np1lem  13574  bitsfzo  13614  sadcaddlem  13636  gcd0id  13690  algcvgblem  13735  prmdvdsexpr  13785  prmfac1  13787  qnumdencl  13800  hashdvds  13833  pcneg  13923  prmpwdvds  13948  prmreclem2  13961  4sqlem12  14000  vdwlem6  14030  vdwlem10  14034  vdwlem13  14037  0ram  14064  ram0  14066  ramz  14069  ramcl  14073  cshwshashlem1  14105  prmlem0  14116  firest  14354  imasaddfnlem  14449  imasvscafn  14458  mremre  14525  drsdirfi  15091  pospo  15126  joinfval  15154  meetfval  15168  lubun  15276  odupos  15288  acsfiindd  15330  psss  15367  symgfix2  15901  f1omvdco2  15934  symggen  15956  odcau  16083  pgpfi  16084  sylow2blem3  16101  sylow3lem2  16107  lsmmod  16152  efgsfo  16216  frgpuptinv  16248  frgpnabllem1  16331  cyggeninv  16340  lt6abl  16351  cyggex2  16353  gsumval3OLD  16362  gsumval3lem2  16364  gsumval3  16365  gsum2d2  16440  dmdprdd  16455  dprd2da  16515  pgpfac1lem5  16554  pgpfac  16559  dvdsrtr  16678  dvdsrmul1  16679  lss1d  16966  lspsolvlem  17145  lspsnat  17148  lbsextlem2  17162  lbsextlem3  17163  domnmuln0  17292  abvn0b  17296  mvrf1  17432  opsrtoslem2  17498  xrsdsreclblem  17703  qsssubdrg  17716  prmirredlem  17759  prmirredlemOLD  17762  cygznlem3  17844  obslbs  17997  dsmmacl  18008  lindfrn  18092  lmiclbs  18108  lmisfree  18113  matecl  18168  mdet1  18250  mdetunilem9  18268  gsummatr01  18307  unitg  18414  tgcl  18416  tgidm  18427  indistopon  18447  fctop  18450  cctop  18452  ppttop  18453  pptbas  18454  epttop  18455  opnnei  18566  neiptopnei  18578  tgrest  18605  restntr  18628  perfopn  18631  ordtrest2lem  18649  isreg2  18823  lmmo  18826  ordthauslem  18829  cmpsublem  18844  cmpsub  18845  cmpcld  18847  hauscmplem  18851  bwthOLD  18856  iunconlem  18873  uncon  18875  2ndcrest  18900  2ndcctbss  18901  2ndcdisj  18902  dis2ndc  18906  txbas  18982  ptbasin  18992  ptbasfi  18996  txcls  19019  txbasval  19021  ptpjopn  19027  ptclsg  19030  dfac14lem  19032  xkoccn  19034  txcnp  19035  txindis  19049  txdis1cn  19050  tx1stc  19065  tx2ndc  19066  txkgen  19067  xkoco1cn  19072  xkoco2cn  19073  xkococn  19075  xkoinjcn  19102  txcon  19104  fbfinnfr  19256  opnfbas  19257  filtop  19270  isfild  19273  fbunfip  19284  filcon  19298  fbasrn  19299  filuni  19300  isufil2  19323  filssufilg  19326  ufileu  19334  filufint  19335  rnelfmlem  19367  rnelfm  19368  fmfnfmlem2  19370  fmfnfmlem4  19372  fmfnfm  19373  hausflimi  19395  hauspwpwf1  19402  flffbas  19410  flftg  19411  alexsublem  19458  alexsubALTlem1  19461  alexsubALTlem2  19462  alexsubALTlem3  19463  alexsubALTlem4  19464  alexsubALT  19465  ptcmplem3  19468  cldsubg  19523  divstgpopn  19532  tgptsmscld  19567  tsmsxplem1  19569  ustfilxp  19629  imasdsf1olem  19790  bldisj  19815  xbln0  19831  prdsxmslem2  19946  xrsblre  20230  icccmplem2  20242  reconn  20247  opnreen  20250  xrge0tsms  20253  metdsre  20271  iccpnfcnv  20358  cnheiborlem  20368  phtpc01  20410  pi1blem  20453  tchcph  20594  cfilfcls  20627  iscau4  20632  bcthlem5  20681  bcth3  20684  hlhil  20772  ovolctb  20815  ovoliunlem2  20828  ovoliunnul  20832  ovolicc2  20847  volfiniun  20870  iundisj  20871  dyadmax  20920  dyadmbllem  20921  vitalilem2  20931  ismbfd  20960  mbfimaopnlem  20975  itg11  21011  i1faddlem  21013  mbfi1fseqlem4  21038  bddmulibl  21158  limciun  21211  perfdvf  21220  rolle  21304  dvivthlem1  21322  dvne0  21325  lhop1  21328  lhop2  21329  itgsubst  21363  pf1ind  21406  dvdsq1p  21517  fta1g  21524  dgrco  21627  plydivex  21648  fta1  21659  ulmcaulem  21744  abelthlem2  21782  pilem2  21802  cxpmul2z  22021  cxpcn3lem  22070  xrlimcnp  22247  jensen  22267  wilthlem2  22292  wilthlem3  22293  muval2  22357  sqf11  22362  ppiublem1  22426  fsumvma  22437  lgsdir2lem2  22548  lgsdir2lem5  22551  dchrisum0fno1  22645  pntlem3  22743  pntleml  22745  ostthlem1  22761  ostth2lem2  22768  colinearalg  22979  axcontlem2  23034  axcontlem8  23040  usgra2edg  23124  usgrares1  23146  nbgraf1olem5  23177  cusgrarn  23190  nbcusgra  23194  uvtxnbgra  23224  3v3e3cycl2  23373  vdusgra0nedg  23401  usgravd0nedg  23405  gxnn0neg  23573  gxnn0suc  23574  lnon0  24021  shmodsi  24615  shlub  24640  spanunsni  24805  h1datomi  24807  stm1ri  25471  stadd3i  25475  mdsl1i  25548  cvmdi  25551  superpos  25581  chjatom  25584  chirredi  25621  atcvat4i  25624  sumdmdii  25642  sumdmdlem  25645  cdj3lem2a  25663  cdj3lem3a  25666  cdj3i  25668  disji2f  25745  disjif2  25749  iundisjf  25755  rnmpt2ss  25816  suppss3  25851  iundisjfi  25903  nn0min  25913  xrge0tsmsd  26106  cnre2csqima  26195  ordtrest2NEWlem  26206  xrge0iifcnv  26217  lmxrge0  26236  measdivcstOLD  26492  dya2iocuni  26552  eulerpartlems  26591  derangenlem  26907  erdszelem9  26935  pconcon  26968  iccllyscon  26987  cvmsval  27003  cvmscld  27010  cvmsss2  27011  cvmopnlem  27015  cvmfolem  27016  cvmliftmolem2  27019  cvmlift2lem10  27049  cvmlift2lem12  27051  cvmlift3lem5  27060  cvmlift3lem8  27063  rtrclreclem.trans  27195  dfrtrcl2  27197  untsucf  27208  3orel1  27213  3orel2  27214  3orel3  27215  nepss  27221  prodmo  27296  fprod2dlem  27338  dfon2lem5  27447  dfon2lem6  27448  dfon2lem7  27449  dfon2lem8  27450  rdgprc  27455  wfi  27515  wfis2fg  27519  trpredtr  27541  dftrpred3g  27544  trpredrec  27549  frmin  27550  frind  27551  frins2fg  27555  wfrlem14  27584  wfrlem15  27585  wsuclem  27609  frrlem5e  27623  nodenselem4  27672  nodenselem8  27676  nocvxmin  27679  nofulllem5  27694  funpartfun  27821  altopth1  27843  altopth2  27844  colineardim1  27939  lineext  27954  btwnconn1lem14  27978  brsegle  27986  hilbert1.2  28033  bpolycl  28042  arg-ax  28110  ordtoplem  28129  onsuct0  28135  fin2so  28260  supaddc  28261  supadd  28262  mblfinlem1  28272  mblfinlem4  28275  ovoliunnfl  28277  itg2addnclem  28287  itg2addnclem2  28288  areacirc  28333  trer  28355  elicc3  28356  finminlem  28357  fneint  28393  fnessref  28409  refssfne  28410  locfincmp  28420  comppfsc  28423  neibastop1  28424  neibastop2lem  28425  neibastop2  28426  fnemeet2  28432  fnejoin2  28434  tailfb  28442  unirep  28450  filbcmb  28478  fzadd2  28481  sdclem1  28483  fdc  28485  nninfnub  28491  isbnd2  28526  ssbnd  28531  prdsbnd2  28538  cntotbnd  28539  heibor1lem  28552  heiborlem1  28554  heiborlem4  28557  heiborlem6  28559  0idl  28669  intidl  28673  unichnidl  28675  keridl  28676  prnc  28711  ceqsex3OLD  28850  prtlem17  28866  prter2  28871  eldioph2b  28946  eldiophss  28958  diophren  28997  ctbnfien  29002  rencldnfilem  29004  pellexlem3  29017  pellexlem5  29019  pellex  29021  pell14qrexpcl  29053  pellfundre  29067  pellfundge  29068  pellfundlb  29070  pellfundglb  29071  jm2.19lem4  29186  fnwe2lem2  29249  pwssplit4  29287  hbtlem5  29329  hirstL-ax3  29752  2reurex  29851  elnelall  29962  ralnralall  29964  otiunsndisj  29978  otiunsndisjX  29979  uzuzle  30036  subsubelfzo0  30056  wwlktovfo  30099  reuccats1  30107  usg2wlkeq  30135  wlkcpr  30136  usgra2pthspth  30141  wlkiswwlksur  30197  clwlkswlks  30269  clwlkisclwwlklem2a4  30292  clwlkisclwwlklem1  30295  clwwlkf1  30304  erclwwlktr0  30325  erclwwlktr  30331  erclwwlkntr  30347  hashecclwwlkn1  30354  usghashecclwwlk  30355  wlkp1lenfislenp  30358  clwlkfoclwwlk  30364  nbhashuvtx  30380  usgravd00  30384  rusgranumwlklem1  30413  3cyclfrgrarn1  30450  frgranbnb  30458  frgrancvvdeqlem3  30471  frgrancvvdeqlem4  30472  frgrancvvdeqlemC  30478  frgrawopreglem3  30485  frgrawopreglem4  30486  frgrawopreglem5  30487  frgrawopreg2  30490  2spotiundisj  30501  2spotmdisj  30507  extwwlkfablem2  30517  numclwwlkun  30518  numclwwlkovf2ex  30525  numclwlk1lem2f1  30533  fmptsnd  30567  ztprmneprm  30583  0rng  30606  01eq0rng  30608  mndpsuppss  30615  lindslinindimp2lem4  30704  lindslinindsimp2  30706  lindsrng01  30711  snlindsntor  30714  ldepspr  30716  isldepslvec2  30728  rng1nfld  30736  onfrALT  30958  ax6e2ndeq  30969  snssiALT  31266  bnj849  31620  bnj1118  31677  bj-sngltag  32059  bj-bary1lem1  32175  lsatn0  32217  lsatcmp  32221  lssat  32234  lfl1  32288  lshpsmreu  32327  lkrin  32382  glbconxN  32595  cvrat4  32660  paddasslem17  33053  pmodlem2  33064  dalawlem14  33101  pclclN  33108  pclfinN  33117  pclfinclN  33167  poml4N  33170  osumcllem8N  33180  pexmidlem5N  33191  cdleme32a  33658  cdlemg33b0  33918  tendoeq2  33991  diaelrnN  34263  dihmeetlem1N  34508  dihglblem5apreN  34509  dihglblem2N  34512  dochvalr  34575  dochkrshp  34604  lcfl6  34718  lcfrvalsnN  34759  mapdordlem2  34855  mapdh8b  34998  mapdh9a  35008  hdmap14lem13  35101
  Copyright terms: Public domain W3C validator