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

Theorem syl5bir 209
Description: A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl5bir.1  |-  ( ps  <->  ph )
syl5bir.2  |-  ( ch 
->  ( ps  ->  th )
)
Assertion
Ref Expression
syl5bir  |-  ( ch 
->  ( ph  ->  th )
)

Proof of Theorem syl5bir
StepHypRef Expression
1 syl5bir.1 . . 3  |-  ( ps  <->  ph )
21biimpri 197 . 2  |-  ( ph  ->  ps )
3 syl5bir.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:  3imtr3g  260  oplem1  930  nic-ax  1428  19.30  1591  19.33b  1595  ax10  1884  necon4bd  2508  ceqex  2898  ssdisj  3504  pssdifn0  3515  disjss3  4022  somo  4348  frminex  4373  ordelord  4414  unizlim  4509  tfinds  4650  tfindsg  4651  tfindes  4653  tfinds2  4654  findsg  4683  sofld  5121  funopfv  5562  mpteqb  5614  suppssr  5659  funfvima  5753  fliftfun  5811  weniso  5852  frxp  6225  rdgsucmptnf  6442  frsucmptn  6451  tz7.49  6457  om00  6573  oewordi  6589  iiner  6731  eroveu  6753  th3qlem1  6764  undom  6950  sdomdif  7009  php3  7047  sucdom2  7057  unxpdomlem3  7069  fisseneq  7074  pssnn  7081  ordunifi  7107  isfinite2  7115  fiint  7133  ixpfi2  7154  finsschain  7162  ordtypelem10  7242  wofib  7260  wemapso2lem  7265  unxpwdom2  7302  sucprcreg  7313  inf3lem2  7330  cantnfp1lem3  7382  cantnfp1  7383  setind  7419  r1tr  7448  r1ordg  7450  rankelb  7496  rankxplim3  7551  cardlim  7605  infxpenlem  7641  infxpenc2  7649  dfac5lem4  7753  dfac12k  7773  kmlem13  7788  sornom  7903  fin23lem25  7950  fin23lem21  7965  zorn2lem4  8126  iundom2g  8162  fpwwe2lem12  8263  fpwwe2lem13  8264  pwfseqlem4a  8283  eltsk2g  8373  inttsk  8396  tskord  8402  r1tskina  8404  grudomon  8439  arch  9962  zaddcl  10059  uzm1  10258  xrsupsslem  10625  xrinfmsslem  10626  fsequb  11037  fseqsupubi  11040  seqf1o  11087  sq01  11223  rexanre  11830  rexuzre  11836  cau3lem  11838  o1co  12060  rlimcn2  12064  o1of2  12086  lo1add  12100  lo1mul  12101  climcau  12144  caucvgb  12152  summo  12190  isumltss  12307  mertenslem2  12341  bitsfzolem  12625  bitsfzo  12626  bezoutlem4  12720  prmind2  12769  isprm5  12791  pcqmul  12906  pcadd  12937  prmreclem2  12964  prmreclem5  12967  mul4sq  13001  vdwmc2  13026  ramcl  13076  prmlem1a  13108  divsfval  13449  iscatd2  13583  catpropd  13612  wunfunc  13773  gaorber  14762  lsmsubm  14964  pj1eu  15005  efgredlem  15056  divsabl  15157  cygabl  15177  cygctb  15178  lt6abl  15181  gsumval3eu  15190  dprdsubg  15259  ablfac1c  15306  pgpfac1  15315  dvdsrtr  15434  unitgrp  15449  drngmul0or  15533  lvecvs0or  15861  lspdisjb  15879  lspsolvlem  15895  lspprat  15906  lbsextlem2  15912  abvn0b  16043  domnchr  16486  znfld  16514  cygznlem3  16523  obselocv  16628  0ntr  16808  opnneiid  16863  restntr  16912  hausnei2  17081  nrmsep3  17083  cmpsub  17127  uncmp  17130  dfcon2  17145  cnconn  17148  1stcfb  17171  txuni2  17260  txbas  17262  ptbasin  17272  txcls  17299  txbasval  17301  txlly  17330  txnlly  17331  pthaus  17332  txlm  17342  tx1stc  17344  xkohaus  17347  isufil2  17603  ufileu  17614  cnpflfi  17694  txflf  17701  fclscf  17720  flimfnfcls  17723  alexsubb  17740  alexsubALTlem2  17742  alexsubALTlem4  17744  ptcmplem2  17747  ptcmplem3  17748  divstgplem  17803  prdsmet  17934  blin2  17975  prdsbl  18037  nmolb  18226  tgqioo  18306  reconnlem2  18332  reconn  18333  lebnumlem3  18461  iscau4  18705  cmetcaulem  18714  iscmet3lem2  18718  bcthlem5  18750  minveclem3b  18792  pmltpc  18810  evthicc2  18820  ovolunlem2  18857  ovolicc2lem5  18880  mblsplit  18891  iundisj2  18906  volsup  18913  ioombl1lem4  18918  dyaddisj  18951  dyadmbllem  18954  i1faddlem  19048  itg10a  19065  itg1ge0a  19066  mbfi1flimlem  19077  mbfmullem  19080  itg2add  19114  rolle  19337  dvcvx  19367  itgsubst  19396  tdeglem4  19446  ply1domn  19509  fta1b  19555  plyadd  19599  plymul  19600  coeeu  19607  vieta1  19692  aalioulem6  19717  ulmcaulem  19771  ulmcau  19772  ulmbdd  19775  ulmcn  19776  amgm  20285  mumullem2  20418  ppiublem1  20441  dchrfi  20494  dchrptlem2  20504  dchrptlem3  20505  dchrsum2  20507  lgsdchr  20587  lgsquad2lem2  20598  2sqlem5  20607  2sqb  20617  pntlemp  20759  ostthlem2  20777  ostth  20788  nvmul0or  21210  ubthlem3  21451  axhcompl-zf  21578  hvmul0or  21604  ocnel  21877  pjhthmo  21881  spanuni  22123  spansni  22136  hon0  22373  leopadd  22712  leoptr  22717  mdsymlem6  22988  sumdmdlem2  22999  cdjreui  23012  ballotlemimin  23064  iundisj2fi  23364  iundisj2f  23366  txscon  23772  cvmsdisj  23801  cvmliftlem15  23829  cvmlift2lem10  23843  cvmlift3lem7  23856  dfon2lem3  24141  dfon2lem5  24143  dfon2lem6  24144  dfon2lem7  24145  dfon2lem8  24146  soseq  24254  frr3g  24280  nodenselem4  24338  nodenselem5  24339  nobndup  24354  nobnddown  24355  funpartfun  24481  axcontlem8  24599  axcontlem9  24600  ifscgr  24667  cgr3tr4  24675  btwnconn1lem13  24722  seglecgr12  24734  isunscov  25074  sssu  25141  svli2  25484  qusp  25542  iintlem1  25610  elicc3  26228  neibastop1  26308  tailfb  26326  fdc  26455  riscer  26619  intidl  26654  ispridlc  26695  prtlem14  26742  prtlem17  26744  diophin  26852  diophun  26853  psgneu  27429  pm10.57  27566  fnchoice  27700  bnj23  28744  bnj594  28944  bnj849  28957  ax12-2  29103  a12studyALT  29133  lpssat  29203  lssatle  29205  lshpkrlem6  29305  cvrnbtwn  29461  atlatmstc  29509  atlatle  29510  atlrelat1  29511  2at0mat0  29714  trlator0  30360  cdleme0moN  30414  cdlemn11pre  31400  dihord2pre  31415  dihmeetlem20N  31516  dochkrshp4  31579  lcfl6  31690
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