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  1640  19.9ht  1738  19.9t  1794  ax12olem5  1884  ax11indn  2147  2euex  2228  necon3bd  2496  necon2ad  2507  necon1ad  2526  pm2.61dne  2536  spcimgft  2872  rspc  2891  rspcimdv  2898  euind  2965  reuind  2981  sbciegft  3034  rspsbc  3082  pwpw0  3779  sssn  3788  eqsn  3791  prel12  3805  pwsnALT  3838  intss1  3893  intmin  3898  uniintsn  3915  iinss  3969  disji2  4026  disjiun  4029  disjxiun  4036  disjss3  4038  trel3  4137  trin  4139  trintss  4145  copsexg  4268  po3nr  4344  fri  4371  wefrc  4403  wereu2  4406  onfr  4447  ord0eln0  4462  trsuc2OLD  4493  onmindif  4498  eusvnfb  4546  reusv3  4558  ssorduni  4593  onmindif2  4619  limuni3  4659  tfis2f  4662  tfinds  4666  tfinds2  4670  tfinds3  4671  frsn  4776  ssrelrel  4803  relop  4850  iss  5014  poirr2  5083  xpcan  5128  xpcan2  5129  sossfld  5136  funopg  5302  funssres  5310  funun  5312  funcnvuni  5333  fv3  5557  fvmptt  5631  iinpreima  5671  suppss  5674  dff3  5689  dff4  5690  fvclss  5776  isomin  5850  isofrlem  5853  f1oweALT  5867  weniso  5868  oprabid  5898  poxp  6243  soxp  6244  fnse  6248  reldmtpos  6258  rntpos  6263  onfununi  6374  smoiun  6394  tfrlem1  6407  tfr3  6431  frsucmptn  6467  tz7.49  6473  oaordi  6560  oawordeulem  6568  omeulem1  6596  oeordi  6601  oelimcl  6614  nnaordi  6632  nneob  6666  omsmolem  6667  erdisj  6723  qsss  6736  th3qlem1  6780  map0g  6823  resixpfo  6870  ixpsnf1o  6872  xpdom3  6976  mapdom3  7049  phplem4  7059  php3  7063  unxpdomlem3  7085  ssfi  7099  findcard2  7114  findcard3  7116  frfi  7118  isfiniteg  7133  xpfi  7144  fiint  7149  finsschain  7178  dffi2  7192  marypha1lem  7202  marypha2  7208  supmo  7219  suplub2  7228  ordiso2  7246  ordtypelem7  7255  ordtypelem8  7256  brwdom2  7303  unxpwdom2  7318  ixpiunwdom  7321  elirrv  7327  suc11reg  7336  noinfep  7376  cantnfle  7388  cantnflem1  7407  cantnf  7411  trcl  7426  epfrs  7429  rankpwi  7511  rankunb  7538  rankuni2b  7541  rankxplim3  7567  cplem1  7575  karden  7581  carddom2  7626  fseqenlem2  7668  ac10ct  7677  acni2  7689  acndom  7694  infpwfien  7705  alephordi  7717  alephord  7718  iunfictbso  7757  aceq3lem  7763  dfac5  7771  dfac2  7773  dfac12lem3  7787  dfac12r  7788  cdainflem  7833  cdainf  7834  cfub  7891  cfeq0  7898  coflim  7903  cfslb2n  7910  cofsmo  7911  coftr  7915  infpssr  7950  fin23lem7  7958  fin23lem11  7959  fin23lem21  7981  isf32lem2  7996  isf34lem4  8019  isfin1-2  8027  isfin1-3  8028  fin1a2lem9  8050  fin1a2lem11  8052  fin1a2lem12  8053  fin1a2lem13  8054  domtriomlem  8084  axdc3lem2  8093  axcclem  8099  ac6c4  8124  zorn2lem4  8142  zorn2lem5  8143  zorn2lem7  8145  ttukeylem5  8156  ttukeyg  8160  brdom6disj  8173  fnrndomg  8176  iunfo  8177  iundom2g  8178  ficard  8203  konigthlem  8206  alephval2  8210  pwcfsdom  8221  fpwwe2lem9  8276  fpwwe2lem11  8278  fpwwe2lem12  8279  fpwwe2lem13  8280  pwfseqlem3  8298  gchpwdom  8312  winalim2  8334  gchina  8337  wunex2  8376  tskr1om2  8406  tskxpss  8410  inar1  8413  tskuni  8421  gruun  8444  grudomon  8455  grur1  8458  ltmpi  8544  ltexprlem2  8677  ltexprlem6  8681  reclem2pr  8688  reclem3pr  8689  reclem4pr  8690  suplem1pr  8692  mulgt0sr  8743  supsrlem  8749  axrrecex  8801  axpre-sup  8807  ltlen  8938  supmul1  9735  supmullem1  9736  supmullem2  9737  supmul  9738  infmrcl  9749  cju  9758  nnsub  9800  un0addcl  10013  un0mulcl  10014  nn0sub  10030  peano5uzi  10116  negn0  10320  zsupss  10323  qbtwnre  10542  xrsupexmnf  10639  xrinfmexpnf  10640  xrsupsslem  10641  xrinfmsslem  10642  xrub  10646  supxrun  10650  xrinfm0  10671  ixxdisj  10687  icodisj  10777  difreicc  10783  flval3  10961  modirr  11025  seqf1o  11103  expcl2lem  11131  expnegz  11152  expaddz  11162  expmulz  11164  facwordi  11318  faclbnd4lem4  11325  bccl  11350  hashfun  11405  hashbclem  11406  hashbc  11407  hashfacen  11408  hashf1lem1  11409  hashf1  11411  wrdind  11493  sqrlem1  11744  sqrlem6  11749  rexanre  11846  cau3lem  11854  2clim  12062  summo  12206  fsum2dlem  12249  fsumiun  12295  rpnnen2  12520  odd2np1lem  12602  bitsfzo  12642  sadcaddlem  12664  gcd0id  12718  algcvgblem  12763  prmdvdsexpr  12811  prmfac1  12813  qnumdencl  12826  hashdvds  12859  pcneg  12942  prmpwdvds  12967  prmreclem2  12980  4sqlem12  13019  vdwlem6  13049  vdwlem10  13053  vdwlem13  13056  0ram  13083  ram0  13085  ramz  13088  ramcl  13092  prmlem0  13123  firest  13353  imasaddfnlem  13446  imasvscafn  13455  mremre  13522  drsdirfi  14088  pospo  14123  lubun  14243  odupos  14255  acsfiindd  14296  psss  14339  odcau  14931  pgpfi  14932  sylow2blem3  14949  sylow3lem2  14955  lsmmod  15000  efgsfo  15064  frgpuptinv  15096  frgpnabllem1  15177  cyggeninv  15186  lt6abl  15197  cyggex2  15199  gsumval3  15207  gsum2d2  15241  dmdprdd  15253  dprd2da  15293  pgpfac1lem5  15330  pgpfac  15335  dvdsrtr  15450  dvdsrmul1  15451  lss1d  15736  lspsolvlem  15911  lspsnat  15914  lbsextlem2  15928  lbsextlem3  15929  domnmuln0  16055  abvn0b  16059  mvrf1  16186  opsrtoslem2  16242  xrsdsreclblem  16433  qsssubdrg  16447  prmirredlem  16462  cygznlem3  16539  obslbs  16646  unitg  16721  tgcl  16723  tgidm  16734  indistopon  16754  fctop  16757  cctop  16759  ppttop  16760  pptbas  16761  epttop  16762  opnnei  16873  tgrest  16906  restntr  16928  perfopn  16931  ordtrest2lem  16949  isreg2  17121  lmmo  17124  ordthauslem  17127  cmpsublem  17142  cmpsub  17143  cmpcld  17145  hauscmplem  17149  iunconlem  17169  uncon  17171  2ndcrest  17196  2ndcctbss  17197  2ndcdisj  17198  dis2ndc  17202  txbas  17278  ptbasin  17288  ptbasfi  17292  txcls  17315  txbasval  17317  ptpjopn  17322  ptclsg  17325  dfac14lem  17327  xkoccn  17329  txcnp  17330  txindis  17344  txdis1cn  17345  tx1stc  17360  tx2ndc  17361  txkgen  17362  xkoco1cn  17367  xkoco2cn  17368  xkococn  17370  xkoinjcn  17397  txcon  17399  fbfinnfr  17552  opnfbas  17553  filtop  17566  isfild  17569  fbunfip  17580  filcon  17594  fbasrn  17595  filuni  17596  isufil2  17619  filssufilg  17622  ufileu  17630  filufint  17631  rnelfmlem  17663  rnelfm  17664  fmfnfmlem2  17666  fmfnfmlem4  17668  fmfnfm  17669  hausflimi  17691  hauspwpwf1  17698  flffbas  17706  flftg  17707  alexsublem  17754  alexsubALTlem1  17757  alexsubALTlem2  17758  alexsubALTlem3  17759  alexsubALTlem4  17760  alexsubALT  17761  ptcmplem3  17764  cldsubg  17809  divstgpopn  17818  tgptsmscld  17849  tsmsxplem1  17851  imasdsf1olem  17953  bldisj  17971  xbln0  17981  prdsxmslem2  18091  xrsblre  18333  icccmplem2  18344  reconn  18349  opnreen  18352  xrge0tsms  18355  metdsre  18373  iccpnfcnv  18458  cnheiborlem  18468  phtpc01  18510  pi1blem  18553  tchcph  18683  cfilfcls  18716  iscau4  18721  bcthlem5  18766  bcth3  18769  hlhil  18823  ovolctb  18865  ovoliunlem2  18878  ovoliunnul  18882  ovolicc2  18897  volfiniun  18920  iundisj  18921  dyadmax  18969  dyadmbllem  18970  vitalilem2  18980  ismbfd  19011  mbfimaopnlem  19026  itg11  19062  i1faddlem  19064  mbfi1fseqlem4  19089  bddmulibl  19209  limciun  19260  perfdvf  19269  rolle  19353  dvivthlem1  19371  dvne0  19374  lhop1  19377  lhop2  19378  itgsubst  19412  pf1ind  19454  dvdsq1p  19562  fta1g  19569  dgrco  19672  plydivex  19693  fta1  19704  ulmcaulem  19787  abelthlem2  19824  pilem2  19844  cxpmul2z  20054  cxpcn3lem  20103  xrlimcnp  20279  jensen  20299  wilthlem2  20323  wilthlem3  20324  muval2  20388  sqf11  20393  ppiublem1  20457  fsumvma  20468  lgsdir2lem2  20579  lgsdir2lem5  20582  dchrisum0fno1  20676  pntlem3  20774  pntleml  20776  ostthlem1  20792  ostth2lem2  20799  gxnn0neg  20946  gxnn0suc  20947  lnon0  21392  shmodsi  21984  shlub  22009  spanunsni  22174  h1datomi  22176  stm1ri  22840  stadd3i  22844  mdsl1i  22917  cvmdi  22920  superpos  22950  chjatom  22953  chirredi  22990  atcvat4i  22993  sumdmdii  23011  sumdmdlem  23014  cdj3lem2a  23032  cdj3lem3a  23035  cdj3i  23037  rnmpt2ss  23254  cnre2csqima  23310  xrge0iifcnv  23330  disji2f  23369  disjif2  23373  iundisjfi  23378  iundisjf  23380  lmxrge0  23390  xrge0tsmsd  23397  sigaclcuni  23494  measdivcstOLD  23566  measdivcst  23567  derangenlem  23717  erdszelem9  23745  pconcon  23777  iccllyscon  23796  cvmsval  23812  cvmscld  23819  cvmsss2  23820  cvmopnlem  23824  cvmfolem  23825  cvmliftmolem2  23828  cvmlift2lem10  23858  cvmlift2lem12  23860  cvmlift3lem5  23869  cvmlift3lem8  23872  rtrclreclem.trans  24058  dfrtrcl2  24060  untsucf  24071  3orel1  24076  3orel2  24077  3orel3  24078  nepss  24087  mulge0b  24101  prodmo  24159  dfon2lem5  24214  dfon2lem6  24215  dfon2lem7  24216  dfon2lem8  24217  rdgprc  24222  wfi  24278  wfis2fg  24282  trpredtr  24304  dftrpred3g  24307  trpredrec  24312  frmin  24313  frind  24314  frins2fg  24318  wfrlem14  24340  wfrlem15  24341  frrlem5e  24360  nodenselem4  24409  nodenselem8  24413  nocvxmin  24416  nofulllem5  24431  funpartfun  24553  altopth1  24571  altopth2  24572  colinearalg  24610  axcontlem2  24665  axcontlem8  24671  colineardim1  24756  lineext  24771  btwnconn1lem14  24795  brsegle  24803  hilbert1.2  24850  bpolycl  24859  arg-ax  24927  ordtoplem  24946  onsuct0  24952  supaddc  24995  supadd  24996  ovoliunnfl  25001  itg2addnclem  25003  itg2addnclem2  25004  itg2addnc  25005  areacirc  25034  nxtor  25088  ltl4ev  25095  untind  25121  uninqs  25142  domrngref  25163  restidsing  25179  repfuntw  25263  inposet  25381  sallnei  25632  nsn  25633  osneisi  25634  qusp  25645  fisub  25657  limptlimpr2lem2  25678  bwt2  25695  addidv2  25760  addcanrg  25770  lineval6a  26192  trer  26330  elicc3  26331  finminlem  26334  fneint  26380  fnessref  26396  refssfne  26397  locfincmp  26407  comppfsc  26410  neibastop1  26411  neibastop2lem  26412  neibastop2  26413  fnemeet2  26419  fnejoin2  26421  tailfb  26429  unirep  26452  filbcmb  26535  fzadd2  26547  sdclem1  26556  fdc  26558  nninfnub  26564  isbnd2  26610  ssbnd  26615  prdsbnd2  26622  cntotbnd  26623  heibor1lem  26636  heiborlem1  26638  heiborlem4  26641  heiborlem6  26643  0idl  26753  intidl  26757  unichnidl  26759  keridl  26760  prnc  26795  ceqsex3OLD  26829  prtlem17  26847  prter2  26852  eldioph2b  26945  eldiophss  26957  diophren  26999  ctbnfien  27004  rencldnfilem  27006  pellexlem3  27019  pellexlem5  27021  pellex  27023  pell14qrexpcl  27055  pellfundre  27069  pellfundge  27070  pellfundlb  27072  pellfundglb  27073  jm2.19lem4  27188  fnwe2lem2  27251  pwssplit4  27294  dsmmacl  27310  lindfrn  27394  lmiclbs  27410  lmisfree  27415  hbtlem5  27435  f1omvdco2  27494  symggen  27514  hirstL-ax3  27963  2reurex  28062  mpt2xopynvov0g  28196  elfznelfzo  28213  injresinj  28215  hashgt12el  28218  hashgt12el2  28219  nbcusgra  28298  uvtxnbgra  28306  3v3e3cycl2  28410  3cyclfrgrarn1  28435  onfrALT  28613  a9e2ndeq  28624  snssiALT  28919  bnj849  29273  bnj1118  29330  a12study5rev  29744  lubunNEW  29785  lsatn0  29811  lsatcmp  29815  lssat  29828  lfl1  29882  lshpsmreu  29921  lkrin  29976  glbconxN  30189  cvrat4  30254  paddasslem17  30647  pmodlem2  30658  dalawlem14  30695  pclclN  30702  pclfinN  30711  pclfinclN  30761  poml4N  30764  osumcllem8N  30774  pexmidlem5N  30785  cdleme32a  31252  cdlemg33b0  31512  tendoeq2  31585  diaelrnN  31857  dihmeetlem1N  32102  dihglblem5apreN  32103  dihglblem2N  32106  dochvalr  32169  dochkrshp  32198  lcfl6  32312  lcfrvalsnN  32353  mapdordlem2  32449  mapdh8b  32592  mapdh9a  32602  hdmap14lem13  32695
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