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

Theorem syl5bir 211
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 199 . 2  |-  ( ph  ->  ps )
3 syl5bir.2 . 2  |-  ( ch 
->  ( ps  ->  th )
)
42, 3syl5 31 1  |-  ( ch 
->  ( ph  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178
This theorem is referenced by:  3imtr3g  262  oplem1  932  nic-ax  1448  19.30  1615  19.33b  1619  hbnt  1800  ax10OLD  2033  necon4bd  2668  ceqex  3068  ssdisj  3679  pssdifn0  3691  disjss3  4213  somo  4539  frminex  4564  ordelord  4605  unizlim  4700  tfinds  4841  tfindsg  4842  tfindes  4844  tfinds2  4845  findsg  4874  sofld  5320  funopfv  5768  mpteqb  5821  suppssr  5866  funfvima  5975  fliftfun  6036  weniso  6077  frxp  6458  rdgsucmptnf  6689  frsucmptn  6698  tz7.49  6704  om00  6820  oewordi  6836  iiner  6978  eroveu  7001  th3qlem1  7012  undom  7198  sdomdif  7257  php3  7295  sucdom2  7305  unxpdomlem3  7317  fisseneq  7322  pssnn  7329  ordunifi  7359  isfinite2  7367  fiint  7385  infssuni  7399  ixpfi2  7407  finsschain  7415  ordtypelem10  7498  wofib  7516  wemapso2lem  7521  unxpwdom2  7558  sucprcreg  7569  inf3lem2  7586  cantnfp1lem3  7638  cantnfp1  7639  setind  7675  r1tr  7704  r1ordg  7706  rankelb  7752  rankxplim3  7807  cardlim  7861  infxpenlem  7897  infxpenc2  7905  dfac5lem4  8009  dfac12k  8029  kmlem13  8044  sornom  8159  fin23lem25  8206  fin23lem21  8221  zorn2lem4  8381  iundom2g  8417  fpwwe2lem12  8518  fpwwe2lem13  8519  pwfseqlem4a  8538  eltsk2g  8628  inttsk  8651  tskord  8657  r1tskina  8659  grudomon  8694  arch  10220  zaddcl  10319  uzm1  10518  xrsupsslem  10887  xrinfmsslem  10888  fsequb  11316  fseqsupubi  11319  seqf1o  11366  sq01  11503  rexanre  12152  rexuzre  12158  cau3lem  12160  o1co  12382  rlimcn2  12386  o1of2  12408  lo1add  12422  lo1mul  12423  climcau  12466  climbdd  12467  caucvgb  12475  summo  12513  isumltss  12630  mertenslem2  12664  bitsfzolem  12948  bitsfzo  12949  bezoutlem4  13043  prmind2  13092  isprm5  13114  pcqmul  13229  pcadd  13260  prmreclem2  13287  prmreclem5  13290  mul4sq  13324  vdwmc2  13349  ramcl  13399  prmlem1a  13431  divsfval  13774  iscatd2  13908  catpropd  13937  wunfunc  14098  gaorber  15087  lsmsubm  15289  pj1eu  15330  efgredlem  15381  divsabl  15482  cygabl  15502  cygctb  15503  lt6abl  15506  gsumval3eu  15515  dprdsubg  15584  ablfac1c  15631  pgpfac1  15640  dvdsrtr  15759  unitgrp  15774  drngmul0or  15858  lvecvs0or  16182  lspdisjb  16200  lspsolvlem  16216  lspprat  16227  lbsextlem2  16233  abvn0b  16364  domnchr  16815  znfld  16843  cygznlem3  16852  obselocv  16957  0ntr  17137  opnneiid  17192  restntr  17248  hausnei2  17419  nrmsep3  17421  cmpsub  17465  uncmp  17468  dfcon2  17484  cnconn  17487  1stcfb  17510  txuni2  17599  txbas  17601  ptbasin  17611  txcls  17638  txbasval  17640  txlly  17670  txnlly  17671  pthaus  17672  txlm  17682  tx1stc  17684  xkohaus  17687  isufil2  17942  ufileu  17953  cnpflfi  18033  txflf  18040  fclscf  18059  flimfnfcls  18062  alexsubb  18079  alexsubALTlem2  18081  alexsubALTlem4  18083  ptcmplem2  18086  ptcmplem3  18087  cnextcn  18100  divstgplem  18152  prdsmet  18402  blin2  18461  prdsbl  18523  nmolb  18753  tgqioo  18833  reconnlem2  18860  reconn  18861  lebnumlem3  18990  iscau4  19234  cmetcaulem  19243  iscmet3lem2  19247  bcthlem5  19283  minveclem3b  19331  pmltpc  19349  evthicc2  19359  ovolunlem2  19396  ovolicc2lem5  19419  mblsplit  19430  iundisj2  19445  volsup  19452  ioombl1lem4  19457  dyaddisj  19490  dyadmbllem  19493  i1faddlem  19587  itg10a  19604  itg1ge0a  19605  mbfi1flimlem  19616  mbfmullem  19619  itg2add  19653  rolle  19876  dvcvx  19906  itgsubst  19935  tdeglem4  19985  ply1domn  20048  fta1b  20094  plyadd  20138  plymul  20139  coeeu  20146  vieta1  20231  aalioulem6  20256  ulmcaulem  20312  ulmcau  20313  ulmbdd  20316  ulmcn  20317  amgm  20831  mumullem2  20965  ppiublem1  20988  dchrfi  21041  dchrptlem2  21051  dchrptlem3  21052  dchrsum2  21054  lgsdchr  21134  lgsquad2lem2  21145  2sqlem5  21154  2sqb  21164  pntlemp  21306  ostthlem2  21324  ostth  21335  usgra2edg  21404  nvmul0or  22135  ubthlem3  22376  axhcompl-zf  22503  hvmul0or  22529  ocnel  22802  pjhthmo  22806  spanuni  23048  spansni  23061  hon0  23298  leopadd  23637  leoptr  23642  mdsymlem6  23913  sumdmdlem2  23924  cdjreui  23937  iundisj2f  24032  iundisj2fi  24155  voliune  24587  volfiniune  24588  ballotlemimin  24765  txscon  24930  cvmsdisj  24959  cvmliftlem15  24987  cvmlift2lem10  25001  cvmlift3lem7  25014  prodmolem2  25263  prodmo  25264  dfon2lem3  25414  dfon2lem5  25416  dfon2lem6  25417  dfon2lem7  25418  dfon2lem8  25419  soseq  25531  frr3g  25583  nodenselem4  25641  nodenselem5  25642  nobndup  25657  nobnddown  25658  axcontlem8  25912  axcontlem9  25913  ifscgr  25980  cgr3tr4  25988  btwnconn1lem13  26035  seglecgr12  26047  ismblfin  26249  itg2addnclem3  26260  ftc1anclem6  26287  elicc3  26322  neibastop1  26390  tailfb  26408  fdc  26451  riscer  26606  intidl  26641  ispridlc  26682  prtlem14  26725  prtlem17  26727  diophin  26833  diophun  26834  psgneu  27408  pm10.57  27545  fnchoice  27678  f0rn0  28081  2ffzoeq  28151  swrdccatin1  28227  2cshwmod  28279  cshw1  28297  cshwssizelem1a  28301  usg2wlkeq  28330  bnj23  29145  bnj594  29345  bnj849  29358  ax10NEW7  29535  lpssat  29873  lssatle  29875  lshpkrlem6  29975  cvrnbtwn  30131  atlatmstc  30179  atlatle  30180  atlrelat1  30181  2at0mat0  30384  trlator0  31030  cdleme0moN  31084  cdlemn11pre  32070  dihord2pre  32085  dihmeetlem20N  32186  dochkrshp4  32249  lcfl6  32360
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 179
  Copyright terms: Public domain W3C validator