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

Theorem syl5bi 208
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 186 . 2  |-  ( ph  ->  ps )
3 syl5bi.2 . 2  |-  ( ch 
->  ( ps  ->  th )
)
42, 3syl5 28 1  |-  ( ch 
->  ( ph  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  3imtr4g  261  ancomsd  440  3jao  1243  sbequ2  1631  19.9ht  1726  19.9t  1782  ax12olem5  1872  ax11indn  2134  2euex  2215  necon3bd  2483  necon2ad  2494  necon1ad  2513  pm2.61dne  2523  spcimgft  2859  rspc  2878  rspcimdv  2885  euind  2952  reuind  2968  sbciegft  3021  rspsbc  3069  pwpw0  3763  sssn  3772  eqsn  3775  prel12  3789  pwsnALT  3822  intss1  3877  intmin  3882  uniintsn  3899  iinss  3953  disji2  4010  disjiun  4013  disjxiun  4020  disjss3  4022  trel3  4121  trin  4123  trintss  4129  copsexg  4252  po3nr  4328  fri  4355  wefrc  4387  wereu2  4390  onfr  4431  ord0eln0  4446  trsuc2OLD  4477  onmindif  4482  eusvnfb  4530  reusv3  4542  ssorduni  4577  onmindif2  4603  limuni3  4643  tfis2f  4646  tfinds  4650  tfinds2  4654  tfinds3  4655  frsn  4760  ssrelrel  4787  relop  4834  iss  4998  poirr2  5067  xpcan  5112  xpcan2  5113  sossfld  5120  funopg  5286  funssres  5294  funun  5296  funcnvuni  5317  fv3  5541  fvmptt  5615  iinpreima  5655  suppss  5658  dff3  5673  dff4  5674  fvclss  5760  isomin  5834  isofrlem  5837  f1oweALT  5851  weniso  5852  oprabid  5882  poxp  6227  soxp  6228  fnse  6232  reldmtpos  6242  rntpos  6247  onfununi  6358  smoiun  6378  tfrlem1  6391  tfr3  6415  frsucmptn  6451  tz7.49  6457  oaordi  6544  oawordeulem  6552  omeulem1  6580  oeordi  6585  oelimcl  6598  nnaordi  6616  nneob  6650  omsmolem  6651  erdisj  6707  qsss  6720  th3qlem1  6764  map0g  6807  resixpfo  6854  ixpsnf1o  6856  xpdom3  6960  mapdom3  7033  phplem4  7043  php3  7047  unxpdomlem3  7069  ssfi  7083  findcard2  7098  findcard3  7100  frfi  7102  isfiniteg  7117  xpfi  7128  fiint  7133  finsschain  7162  dffi2  7176  marypha1lem  7186  marypha2  7192  supmo  7203  suplub2  7212  ordiso2  7230  ordtypelem7  7239  ordtypelem8  7240  brwdom2  7287  unxpwdom2  7302  ixpiunwdom  7305  elirrv  7311  suc11reg  7320  noinfep  7360  cantnfle  7372  cantnflem1  7391  cantnf  7395  trcl  7410  epfrs  7413  rankpwi  7495  rankunb  7522  rankuni2b  7525  rankxplim3  7551  cplem1  7559  karden  7565  carddom2  7610  fseqenlem2  7652  ac10ct  7661  acni2  7673  acndom  7678  infpwfien  7689  alephordi  7701  alephord  7702  iunfictbso  7741  aceq3lem  7747  dfac5  7755  dfac2  7757  dfac12lem3  7771  dfac12r  7772  cdainflem  7817  cdainf  7818  cfub  7875  cfeq0  7882  coflim  7887  cfslb2n  7894  cofsmo  7895  coftr  7899  infpssr  7934  fin23lem7  7942  fin23lem11  7943  fin23lem21  7965  isf32lem2  7980  isf34lem4  8003  isfin1-2  8011  isfin1-3  8012  fin1a2lem9  8034  fin1a2lem11  8036  fin1a2lem12  8037  fin1a2lem13  8038  domtriomlem  8068  axdc3lem2  8077  axcclem  8083  ac6c4  8108  zorn2lem4  8126  zorn2lem5  8127  zorn2lem7  8129  ttukeylem5  8140  ttukeyg  8144  brdom6disj  8157  fnrndomg  8160  iunfo  8161  iundom2g  8162  ficard  8187  konigthlem  8190  alephval2  8194  pwcfsdom  8205  fpwwe2lem9  8260  fpwwe2lem11  8262  fpwwe2lem12  8263  fpwwe2lem13  8264  pwfseqlem3  8282  gchpwdom  8296  winalim2  8318  gchina  8321  wunex2  8360  tskr1om2  8390  tskxpss  8394  inar1  8397  tskuni  8405  gruun  8428  grudomon  8439  grur1  8442  ltmpi  8528  ltexprlem2  8661  ltexprlem6  8665  reclem2pr  8672  reclem3pr  8673  reclem4pr  8674  suplem1pr  8676  mulgt0sr  8727  supsrlem  8733  axrrecex  8785  axpre-sup  8791  ltlen  8922  supmul1  9719  supmullem1  9720  supmullem2  9721  supmul  9722  infmrcl  9733  cju  9742  nnsub  9784  un0addcl  9997  un0mulcl  9998  nn0sub  10014  peano5uzi  10100  negn0  10304  zsupss  10307  qbtwnre  10526  xrsupexmnf  10623  xrinfmexpnf  10624  xrsupsslem  10625  xrinfmsslem  10626  xrub  10630  supxrun  10634  xrinfm0  10655  ixxdisj  10671  icodisj  10761  difreicc  10767  flval3  10945  modirr  11009  seqf1o  11087  expcl2lem  11115  expnegz  11136  expaddz  11146  expmulz  11148  facwordi  11302  faclbnd4lem4  11309  bccl  11334  hashfun  11389  hashbclem  11390  hashbc  11391  hashfacen  11392  hashf1lem1  11393  hashf1  11395  wrdind  11477  sqrlem1  11728  sqrlem6  11733  rexanre  11830  cau3lem  11838  2clim  12046  summo  12190  fsum2dlem  12233  fsumiun  12279  rpnnen2  12504  odd2np1lem  12586  bitsfzo  12626  sadcaddlem  12648  gcd0id  12702  algcvgblem  12747  prmdvdsexpr  12795  prmfac1  12797  qnumdencl  12810  hashdvds  12843  pcneg  12926  prmpwdvds  12951  prmreclem2  12964  4sqlem12  13003  vdwlem6  13033  vdwlem10  13037  vdwlem13  13040  0ram  13067  ram0  13069  ramz  13072  ramcl  13076  prmlem0  13107  firest  13337  imasaddfnlem  13430  imasvscafn  13439  mremre  13506  drsdirfi  14072  pospo  14107  lubun  14227  odupos  14239  acsfiindd  14280  psss  14323  odcau  14915  pgpfi  14916  sylow2blem3  14933  sylow3lem2  14939  lsmmod  14984  efgsfo  15048  frgpuptinv  15080  frgpnabllem1  15161  cyggeninv  15170  lt6abl  15181  cyggex2  15183  gsumval3  15191  gsum2d2  15225  dmdprdd  15237  dprd2da  15277  pgpfac1lem5  15314  pgpfac  15319  dvdsrtr  15434  dvdsrmul1  15435  lss1d  15720  lspsolvlem  15895  lspsnat  15898  lbsextlem2  15912  lbsextlem3  15913  domnmuln0  16039  abvn0b  16043  mvrf1  16170  opsrtoslem2  16226  xrsdsreclblem  16417  qsssubdrg  16431  prmirredlem  16446  cygznlem3  16523  obslbs  16630  unitg  16705  tgcl  16707  tgidm  16718  indistopon  16738  fctop  16741  cctop  16743  ppttop  16744  pptbas  16745  epttop  16746  opnnei  16857  tgrest  16890  restntr  16912  perfopn  16915  ordtrest2lem  16933  isreg2  17105  lmmo  17108  ordthauslem  17111  cmpsublem  17126  cmpsub  17127  cmpcld  17129  hauscmplem  17133  iunconlem  17153  uncon  17155  2ndcrest  17180  2ndcctbss  17181  2ndcdisj  17182  dis2ndc  17186  txbas  17262  ptbasin  17272  ptbasfi  17276  txcls  17299  txbasval  17301  ptpjopn  17306  ptclsg  17309  dfac14lem  17311  xkoccn  17313  txcnp  17314  txindis  17328  txdis1cn  17329  tx1stc  17344  tx2ndc  17345  txkgen  17346  xkoco1cn  17351  xkoco2cn  17352  xkococn  17354  xkoinjcn  17381  txcon  17383  fbfinnfr  17536  opnfbas  17537  filtop  17550  isfild  17553  fbunfip  17564  filcon  17578  fbasrn  17579  filuni  17580  isufil2  17603  filssufilg  17606  ufileu  17614  filufint  17615  rnelfmlem  17647  rnelfm  17648  fmfnfmlem2  17650  fmfnfmlem4  17652  fmfnfm  17653  hausflimi  17675  hauspwpwf1  17682  flffbas  17690  flftg  17691  alexsublem  17738  alexsubALTlem1  17741  alexsubALTlem2  17742  alexsubALTlem3  17743  alexsubALTlem4  17744  alexsubALT  17745  ptcmplem3  17748  cldsubg  17793  divstgpopn  17802  tgptsmscld  17833  tsmsxplem1  17835  imasdsf1olem  17937  bldisj  17955  xbln0  17965  prdsxmslem2  18075  xrsblre  18317  icccmplem2  18328  reconn  18333  opnreen  18336  xrge0tsms  18339  metdsre  18357  iccpnfcnv  18442  cnheiborlem  18452  phtpc01  18494  pi1blem  18537  tchcph  18667  cfilfcls  18700  iscau4  18705  bcthlem5  18750  bcth3  18753  hlhil  18807  ovolctb  18849  ovoliunlem2  18862  ovoliunnul  18866  ovolicc2  18881  volfiniun  18904  iundisj  18905  dyadmax  18953  dyadmbllem  18954  vitalilem2  18964  ismbfd  18995  mbfimaopnlem  19010  itg11  19046  i1faddlem  19048  mbfi1fseqlem4  19073  bddmulibl  19193  limciun  19244  perfdvf  19253  rolle  19337  dvivthlem1  19355  dvne0  19358  lhop1  19361  lhop2  19362  itgsubst  19396  pf1ind  19438  dvdsq1p  19546  fta1g  19553  dgrco  19656  plydivex  19677  fta1  19688  ulmcaulem  19771  abelthlem2  19808  pilem2  19828  cxpmul2z  20038  cxpcn3lem  20087  xrlimcnp  20263  jensen  20283  wilthlem2  20307  wilthlem3  20308  muval2  20372  sqf11  20377  ppiublem1  20441  fsumvma  20452  lgsdir2lem2  20563  lgsdir2lem5  20566  dchrisum0fno1  20660  pntlem3  20758  pntleml  20760  ostthlem1  20776  ostth2lem2  20783  gxnn0neg  20930  gxnn0suc  20931  lnon0  21376  shmodsi  21968  shlub  21993  spanunsni  22158  h1datomi  22160  stm1ri  22824  stadd3i  22828  mdsl1i  22901  cvmdi  22904  superpos  22934  chjatom  22937  chirredi  22974  atcvat4i  22977  sumdmdii  22995  sumdmdlem  22998  cdj3lem2a  23016  cdj3lem3a  23019  cdj3i  23021  rnmpt2ss  23239  cnre2csqima  23295  xrge0iifcnv  23315  disji2f  23354  disjif2  23358  iundisjfi  23363  iundisjf  23365  lmxrge0  23375  xrge0tsmsd  23382  sigaclcuni  23479  measdivcstOLD  23551  measdivcst  23552  derangenlem  23702  erdszelem9  23730  pconcon  23762  iccllyscon  23781  cvmsval  23797  cvmscld  23804  cvmsss2  23805  cvmopnlem  23809  cvmfolem  23810  cvmliftmolem2  23813  cvmlift2lem10  23843  cvmlift2lem12  23845  cvmlift3lem5  23854  cvmlift3lem8  23857  rtrclreclem.trans  24043  dfrtrcl2  24045  untsucf  24056  3orel1  24061  3orel2  24062  3orel3  24063  nepss  24072  mulge0b  24086  dfon2lem5  24143  dfon2lem6  24144  dfon2lem7  24145  dfon2lem8  24146  rdgprc  24151  wfi  24207  wfis2fg  24211  trpredtr  24233  dftrpred3g  24236  trpredrec  24241  frmin  24242  frind  24243  frins2fg  24247  wfrlem14  24269  wfrlem15  24270  frrlem5e  24289  nodenselem4  24338  nodenselem8  24342  nocvxmin  24345  nofulllem5  24360  funpartfv  24483  altopth1  24499  altopth2  24500  colinearalg  24538  axcontlem2  24593  axcontlem8  24599  colineardim1  24684  lineext  24699  btwnconn1lem14  24723  brsegle  24731  hilbert1.2  24778  bpolycl  24787  arg-ax  24855  ordtoplem  24874  onsuct0  24880  areacirc  24931  nxtor  24985  ltl4ev  24992  untind  25018  uninqs  25039  domrngref  25060  restidsing  25076  repfuntw  25160  inposet  25278  sallnei  25529  nsn  25530  osneisi  25531  qusp  25542  fisub  25554  limptlimpr2lem2  25575  bwt2  25592  addidv2  25657  addcanrg  25667  lineval6a  26089  trer  26227  elicc3  26228  finminlem  26231  fneint  26277  fnessref  26293  refssfne  26294  locfincmp  26304  comppfsc  26307  neibastop1  26308  neibastop2lem  26309  neibastop2  26310  fnemeet2  26316  fnejoin2  26318  tailfb  26326  unirep  26349  filbcmb  26432  fzadd2  26444  sdclem1  26453  fdc  26455  nninfnub  26461  isbnd2  26507  ssbnd  26512  prdsbnd2  26519  cntotbnd  26520  heibor1lem  26533  heiborlem1  26535  heiborlem4  26538  heiborlem6  26540  0idl  26650  intidl  26654  unichnidl  26656  keridl  26657  prnc  26692  ceqsex3OLD  26726  prtlem17  26744  prter2  26749  eldioph2b  26842  eldiophss  26854  diophren  26896  ctbnfien  26901  rencldnfilem  26903  pellexlem3  26916  pellexlem5  26918  pellex  26920  pell14qrexpcl  26952  pellfundre  26966  pellfundge  26967  pellfundlb  26969  pellfundglb  26970  jm2.19lem4  27085  fnwe2lem2  27148  pwssplit4  27191  dsmmacl  27207  lindfrn  27291  lmiclbs  27307  lmisfree  27312  hbtlem5  27332  f1omvdco2  27391  symggen  27411  hirstL-ax3  27860  2reurex  27959  mpt2xopynvov0g  28080  nbcusgra  28159  uvtxnbgra  28165  onfrALT  28314  a9e2ndeq  28325  snssiALT  28603  bnj849  28957  bnj1118  29014  a12study5rev  29122  lubunNEW  29163  lsatn0  29189  lsatcmp  29193  lssat  29206  lfl1  29260  lshpsmreu  29299  lkrin  29354  glbconxN  29567  cvrat4  29632  paddasslem17  30025  pmodlem2  30036  dalawlem14  30073  pclclN  30080  pclfinN  30089  pclfinclN  30139  poml4N  30142  osumcllem8N  30152  pexmidlem5N  30163  cdleme32a  30630  cdlemg33b0  30890  tendoeq2  30963  diaelrnN  31235  dihmeetlem1N  31480  dihglblem5apreN  31481  dihglblem2N  31484  dochvalr  31547  dochkrshp  31576  lcfl6  31690  lcfrvalsnN  31731  mapdordlem2  31827  mapdh8b  31970  mapdh9a  31980  hdmap14lem13  32073
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator