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  1633  19.9ht  1728  19.9t  1784  ax12olem5  1874  ax11indn  2136  2euex  2217  necon3bd  2485  necon2ad  2496  necon1ad  2515  pm2.61dne  2525  spcimgft  2861  rspc  2880  rspcimdv  2887  euind  2954  reuind  2970  sbciegft  3023  rspsbc  3071  pwpw0  3765  sssn  3774  eqsn  3777  prel12  3791  pwsnALT  3824  intss1  3879  intmin  3884  uniintsn  3901  iinss  3955  disji2  4012  disjiun  4015  disjxiun  4022  disjss3  4024  trel3  4123  trin  4125  trintss  4131  copsexg  4254  po3nr  4330  fri  4357  wefrc  4389  wereu2  4392  onfr  4433  ord0eln0  4448  trsuc2OLD  4479  onmindif  4484  eusvnfb  4532  reusv3  4544  ssorduni  4579  onmindif2  4605  limuni3  4645  tfis2f  4648  tfinds  4652  tfinds2  4656  tfinds3  4657  frsn  4762  ssrelrel  4789  relop  4836  iss  5000  poirr2  5069  xpcan  5114  xpcan2  5115  sossfld  5122  funopg  5288  funssres  5296  funun  5298  funcnvuni  5319  fv3  5543  fvmptt  5617  iinpreima  5657  suppss  5660  dff3  5675  dff4  5676  fvclss  5762  isomin  5836  isofrlem  5839  f1oweALT  5853  weniso  5854  oprabid  5884  poxp  6229  soxp  6230  fnse  6234  reldmtpos  6244  rntpos  6249  onfununi  6360  smoiun  6380  tfrlem1  6393  tfr3  6417  frsucmptn  6453  tz7.49  6459  oaordi  6546  oawordeulem  6554  omeulem1  6582  oeordi  6587  oelimcl  6600  nnaordi  6618  nneob  6652  omsmolem  6653  erdisj  6709  qsss  6722  th3qlem1  6766  map0g  6809  resixpfo  6856  ixpsnf1o  6858  xpdom3  6962  mapdom3  7035  phplem4  7045  php3  7049  unxpdomlem3  7071  ssfi  7085  findcard2  7100  findcard3  7102  frfi  7104  isfiniteg  7119  xpfi  7130  fiint  7135  finsschain  7164  dffi2  7178  marypha1lem  7188  marypha2  7194  supmo  7205  suplub2  7214  ordiso2  7232  ordtypelem7  7241  ordtypelem8  7242  brwdom2  7289  unxpwdom2  7304  ixpiunwdom  7307  elirrv  7313  suc11reg  7322  noinfep  7362  cantnfle  7374  cantnflem1  7393  cantnf  7397  trcl  7412  epfrs  7415  rankpwi  7497  rankunb  7524  rankuni2b  7527  rankxplim3  7553  cplem1  7561  karden  7567  carddom2  7612  fseqenlem2  7654  ac10ct  7663  acni2  7675  acndom  7680  infpwfien  7691  alephordi  7703  alephord  7704  iunfictbso  7743  aceq3lem  7749  dfac5  7757  dfac2  7759  dfac12lem3  7773  dfac12r  7774  cdainflem  7819  cdainf  7820  cfub  7877  cfeq0  7884  coflim  7889  cfslb2n  7896  cofsmo  7897  coftr  7901  infpssr  7936  fin23lem7  7944  fin23lem11  7945  fin23lem21  7967  isf32lem2  7982  isf34lem4  8005  isfin1-2  8013  isfin1-3  8014  fin1a2lem9  8036  fin1a2lem11  8038  fin1a2lem12  8039  fin1a2lem13  8040  domtriomlem  8070  axdc3lem2  8079  axcclem  8085  ac6c4  8110  zorn2lem4  8128  zorn2lem5  8129  zorn2lem7  8131  ttukeylem5  8142  ttukeyg  8146  brdom6disj  8159  fnrndomg  8162  iunfo  8163  iundom2g  8164  ficard  8189  konigthlem  8192  alephval2  8196  pwcfsdom  8207  fpwwe2lem9  8262  fpwwe2lem11  8264  fpwwe2lem12  8265  fpwwe2lem13  8266  pwfseqlem3  8284  gchpwdom  8298  winalim2  8320  gchina  8323  wunex2  8362  tskr1om2  8392  tskxpss  8396  inar1  8399  tskuni  8407  gruun  8430  grudomon  8441  grur1  8444  ltmpi  8530  ltexprlem2  8663  ltexprlem6  8667  reclem2pr  8674  reclem3pr  8675  reclem4pr  8676  suplem1pr  8678  mulgt0sr  8729  supsrlem  8735  axrrecex  8787  axpre-sup  8793  ltlen  8924  supmul1  9721  supmullem1  9722  supmullem2  9723  supmul  9724  infmrcl  9735  cju  9744  nnsub  9786  un0addcl  9999  un0mulcl  10000  nn0sub  10016  peano5uzi  10102  negn0  10306  zsupss  10309  qbtwnre  10528  xrsupexmnf  10625  xrinfmexpnf  10626  xrsupsslem  10627  xrinfmsslem  10628  xrub  10632  supxrun  10636  xrinfm0  10657  ixxdisj  10673  icodisj  10763  difreicc  10769  flval3  10947  modirr  11011  seqf1o  11089  expcl2lem  11117  expnegz  11138  expaddz  11148  expmulz  11150  facwordi  11304  faclbnd4lem4  11311  bccl  11336  hashfun  11391  hashbclem  11392  hashbc  11393  hashfacen  11394  hashf1lem1  11395  hashf1  11397  wrdind  11479  sqrlem1  11730  sqrlem6  11735  rexanre  11832  cau3lem  11840  2clim  12048  summo  12192  fsum2dlem  12235  fsumiun  12281  rpnnen2  12506  odd2np1lem  12588  bitsfzo  12628  sadcaddlem  12650  gcd0id  12704  algcvgblem  12749  prmdvdsexpr  12797  prmfac1  12799  qnumdencl  12812  hashdvds  12845  pcneg  12928  prmpwdvds  12953  prmreclem2  12966  4sqlem12  13005  vdwlem6  13035  vdwlem10  13039  vdwlem13  13042  0ram  13069  ram0  13071  ramz  13074  ramcl  13078  prmlem0  13109  firest  13339  imasaddfnlem  13432  imasvscafn  13441  mremre  13508  drsdirfi  14074  pospo  14109  lubun  14229  odupos  14241  acsfiindd  14282  psss  14325  odcau  14917  pgpfi  14918  sylow2blem3  14935  sylow3lem2  14941  lsmmod  14986  efgsfo  15050  frgpuptinv  15082  frgpnabllem1  15163  cyggeninv  15172  lt6abl  15183  cyggex2  15185  gsumval3  15193  gsum2d2  15227  dmdprdd  15239  dprd2da  15279  pgpfac1lem5  15316  pgpfac  15321  dvdsrtr  15436  dvdsrmul1  15437  lss1d  15722  lspsolvlem  15897  lspsnat  15900  lbsextlem2  15914  lbsextlem3  15915  domnmuln0  16041  abvn0b  16045  mvrf1  16172  opsrtoslem2  16228  xrsdsreclblem  16419  qsssubdrg  16433  prmirredlem  16448  cygznlem3  16525  obslbs  16632  unitg  16707  tgcl  16709  tgidm  16720  indistopon  16740  fctop  16743  cctop  16745  ppttop  16746  pptbas  16747  epttop  16748  opnnei  16859  tgrest  16892  restntr  16914  perfopn  16917  ordtrest2lem  16935  isreg2  17107  lmmo  17110  ordthauslem  17113  cmpsublem  17128  cmpsub  17129  cmpcld  17131  hauscmplem  17135  iunconlem  17155  uncon  17157  2ndcrest  17182  2ndcctbss  17183  2ndcdisj  17184  dis2ndc  17188  txbas  17264  ptbasin  17274  ptbasfi  17278  txcls  17301  txbasval  17303  ptpjopn  17308  ptclsg  17311  dfac14lem  17313  xkoccn  17315  txcnp  17316  txindis  17330  txdis1cn  17331  tx1stc  17346  tx2ndc  17347  txkgen  17348  xkoco1cn  17353  xkoco2cn  17354  xkococn  17356  xkoinjcn  17383  txcon  17385  fbfinnfr  17538  opnfbas  17539  filtop  17552  isfild  17555  fbunfip  17566  filcon  17580  fbasrn  17581  filuni  17582  isufil2  17605  filssufilg  17608  ufileu  17616  filufint  17617  rnelfmlem  17649  rnelfm  17650  fmfnfmlem2  17652  fmfnfmlem4  17654  fmfnfm  17655  hausflimi  17677  hauspwpwf1  17684  flffbas  17692  flftg  17693  alexsublem  17740  alexsubALTlem1  17743  alexsubALTlem2  17744  alexsubALTlem3  17745  alexsubALTlem4  17746  alexsubALT  17747  ptcmplem3  17750  cldsubg  17795  divstgpopn  17804  tgptsmscld  17835  tsmsxplem1  17837  imasdsf1olem  17939  bldisj  17957  xbln0  17967  prdsxmslem2  18077  xrsblre  18319  icccmplem2  18330  reconn  18335  opnreen  18338  xrge0tsms  18341  metdsre  18359  iccpnfcnv  18444  cnheiborlem  18454  phtpc01  18496  pi1blem  18539  tchcph  18669  cfilfcls  18702  iscau4  18707  bcthlem5  18752  bcth3  18755  hlhil  18809  ovolctb  18851  ovoliunlem2  18864  ovoliunnul  18868  ovolicc2  18883  volfiniun  18906  iundisj  18907  dyadmax  18955  dyadmbllem  18956  vitalilem2  18966  ismbfd  18997  mbfimaopnlem  19012  itg11  19048  i1faddlem  19050  mbfi1fseqlem4  19075  bddmulibl  19195  limciun  19246  perfdvf  19255  rolle  19339  dvivthlem1  19357  dvne0  19360  lhop1  19363  lhop2  19364  itgsubst  19398  pf1ind  19440  dvdsq1p  19548  fta1g  19555  dgrco  19658  plydivex  19679  fta1  19690  ulmcaulem  19773  abelthlem2  19810  pilem2  19830  cxpmul2z  20040  cxpcn3lem  20089  xrlimcnp  20265  jensen  20285  wilthlem2  20309  wilthlem3  20310  muval2  20374  sqf11  20379  ppiublem1  20443  fsumvma  20454  lgsdir2lem2  20565  lgsdir2lem5  20568  dchrisum0fno1  20662  pntlem3  20760  pntleml  20762  ostthlem1  20778  ostth2lem2  20785  gxnn0neg  20932  gxnn0suc  20933  lnon0  21378  shmodsi  21970  shlub  21995  spanunsni  22160  h1datomi  22162  stm1ri  22826  stadd3i  22830  mdsl1i  22903  cvmdi  22906  superpos  22936  chjatom  22939  chirredi  22976  atcvat4i  22979  sumdmdii  22997  sumdmdlem  23000  cdj3lem2a  23018  cdj3lem3a  23021  cdj3i  23023  rnmpt2ss  23241  cnre2csqima  23297  xrge0iifcnv  23317  disji2f  23356  disjif2  23360  iundisjfi  23365  iundisjf  23367  lmxrge0  23377  xrge0tsmsd  23384  sigaclcuni  23481  measdivcstOLD  23553  measdivcst  23554  derangenlem  23704  erdszelem9  23732  pconcon  23764  iccllyscon  23783  cvmsval  23799  cvmscld  23806  cvmsss2  23807  cvmopnlem  23811  cvmfolem  23812  cvmliftmolem2  23815  cvmlift2lem10  23845  cvmlift2lem12  23847  cvmlift3lem5  23856  cvmlift3lem8  23859  rtrclreclem.trans  24045  dfrtrcl2  24047  untsucf  24058  3orel1  24063  3orel2  24064  3orel3  24065  nepss  24074  mulge0b  24088  dfon2lem5  24145  dfon2lem6  24146  dfon2lem7  24147  dfon2lem8  24148  rdgprc  24153  wfi  24209  wfis2fg  24213  trpredtr  24235  dftrpred3g  24238  trpredrec  24243  frmin  24244  frind  24245  frins2fg  24249  wfrlem14  24271  wfrlem15  24272  frrlem5e  24291  nodenselem4  24340  nodenselem8  24344  nocvxmin  24347  nofulllem5  24362  funpartfv  24485  altopth1  24501  altopth2  24502  colinearalg  24540  axcontlem2  24595  axcontlem8  24601  colineardim1  24686  lineext  24701  btwnconn1lem14  24725  brsegle  24733  hilbert1.2  24780  bpolycl  24789  arg-ax  24857  ordtoplem  24876  onsuct0  24882  supaddc  24927  supadd  24928  itg2addnclem  24933  itg2addnclem2  24934  itg2addnc  24935  areacirc  24942  nxtor  24996  ltl4ev  25003  untind  25029  uninqs  25050  domrngref  25071  restidsing  25087  repfuntw  25171  inposet  25289  sallnei  25540  nsn  25541  osneisi  25542  qusp  25553  fisub  25565  limptlimpr2lem2  25586  bwt2  25603  addidv2  25668  addcanrg  25678  lineval6a  26100  trer  26238  elicc3  26239  finminlem  26242  fneint  26288  fnessref  26304  refssfne  26305  locfincmp  26315  comppfsc  26318  neibastop1  26319  neibastop2lem  26320  neibastop2  26321  fnemeet2  26327  fnejoin2  26329  tailfb  26337  unirep  26360  filbcmb  26443  fzadd2  26455  sdclem1  26464  fdc  26466  nninfnub  26472  isbnd2  26518  ssbnd  26523  prdsbnd2  26530  cntotbnd  26531  heibor1lem  26544  heiborlem1  26546  heiborlem4  26549  heiborlem6  26551  0idl  26661  intidl  26665  unichnidl  26667  keridl  26668  prnc  26703  ceqsex3OLD  26737  prtlem17  26755  prter2  26760  eldioph2b  26853  eldiophss  26865  diophren  26907  ctbnfien  26912  rencldnfilem  26914  pellexlem3  26927  pellexlem5  26929  pellex  26931  pell14qrexpcl  26963  pellfundre  26977  pellfundge  26978  pellfundlb  26980  pellfundglb  26981  jm2.19lem4  27096  fnwe2lem2  27159  pwssplit4  27202  dsmmacl  27218  lindfrn  27302  lmiclbs  27318  lmisfree  27323  hbtlem5  27343  f1omvdco2  27402  symggen  27422  hirstL-ax3  27871  2reurex  27970  mpt2xopynvov0g  28091  nbcusgra  28170  uvtxnbgra  28176  onfrALT  28370  a9e2ndeq  28381  snssiALT  28676  bnj849  29030  bnj1118  29087  a12study5rev  29195  lubunNEW  29236  lsatn0  29262  lsatcmp  29266  lssat  29279  lfl1  29333  lshpsmreu  29372  lkrin  29427  glbconxN  29640  cvrat4  29705  paddasslem17  30098  pmodlem2  30109  dalawlem14  30146  pclclN  30153  pclfinN  30162  pclfinclN  30212  poml4N  30215  osumcllem8N  30225  pexmidlem5N  30236  cdleme32a  30703  cdlemg33b0  30963  tendoeq2  31036  diaelrnN  31308  dihmeetlem1N  31553  dihglblem5apreN  31554  dihglblem2N  31557  dochvalr  31620  dochkrshp  31649  lcfl6  31763  lcfrvalsnN  31804  mapdordlem2  31900  mapdh8b  32043  mapdh9a  32053  hdmap14lem13  32146
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