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

Theorem syl5bir 210
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 198 . 2  |-  ( ph  ->  ps )
3 syl5bir.2 . 2  |-  ( ch 
->  ( ps  ->  th )
)
42, 3syl5 30 1  |-  ( ch 
->  ( ph  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  3imtr3g  261  oplem1  931  nic-ax  1447  19.30  1614  19.33b  1618  hbnt  1799  ax10OLD  2032  necon4bd  2660  ceqex  3058  ssdisj  3669  pssdifn0  3681  disjss3  4203  somo  4529  frminex  4554  ordelord  4595  unizlim  4690  tfinds  4831  tfindsg  4832  tfindes  4834  tfinds2  4835  findsg  4864  sofld  5310  funopfv  5758  mpteqb  5811  suppssr  5856  funfvima  5965  fliftfun  6026  weniso  6067  frxp  6448  rdgsucmptnf  6679  frsucmptn  6688  tz7.49  6694  om00  6810  oewordi  6826  iiner  6968  eroveu  6991  th3qlem1  7002  undom  7188  sdomdif  7247  php3  7285  sucdom2  7295  unxpdomlem3  7307  fisseneq  7312  pssnn  7319  ordunifi  7349  isfinite2  7357  fiint  7375  infssuni  7389  ixpfi2  7397  finsschain  7405  ordtypelem10  7488  wofib  7506  wemapso2lem  7511  unxpwdom2  7548  sucprcreg  7559  inf3lem2  7576  cantnfp1lem3  7628  cantnfp1  7629  setind  7665  r1tr  7694  r1ordg  7696  rankelb  7742  rankxplim3  7797  cardlim  7851  infxpenlem  7887  infxpenc2  7895  dfac5lem4  7999  dfac12k  8019  kmlem13  8034  sornom  8149  fin23lem25  8196  fin23lem21  8211  zorn2lem4  8371  iundom2g  8407  fpwwe2lem12  8508  fpwwe2lem13  8509  pwfseqlem4a  8528  eltsk2g  8618  inttsk  8641  tskord  8647  r1tskina  8649  grudomon  8684  arch  10210  zaddcl  10309  uzm1  10508  xrsupsslem  10877  xrinfmsslem  10878  fsequb  11306  fseqsupubi  11309  seqf1o  11356  sq01  11493  rexanre  12142  rexuzre  12148  cau3lem  12150  o1co  12372  rlimcn2  12376  o1of2  12398  lo1add  12412  lo1mul  12413  climcau  12456  climbdd  12457  caucvgb  12465  summo  12503  isumltss  12620  mertenslem2  12654  bitsfzolem  12938  bitsfzo  12939  bezoutlem4  13033  prmind2  13082  isprm5  13104  pcqmul  13219  pcadd  13250  prmreclem2  13277  prmreclem5  13280  mul4sq  13314  vdwmc2  13339  ramcl  13389  prmlem1a  13421  divsfval  13764  iscatd2  13898  catpropd  13927  wunfunc  14088  gaorber  15077  lsmsubm  15279  pj1eu  15320  efgredlem  15371  divsabl  15472  cygabl  15492  cygctb  15493  lt6abl  15496  gsumval3eu  15505  dprdsubg  15574  ablfac1c  15621  pgpfac1  15630  dvdsrtr  15749  unitgrp  15764  drngmul0or  15848  lvecvs0or  16172  lspdisjb  16190  lspsolvlem  16206  lspprat  16217  lbsextlem2  16223  abvn0b  16354  domnchr  16805  znfld  16833  cygznlem3  16842  obselocv  16947  0ntr  17127  opnneiid  17182  restntr  17238  hausnei2  17409  nrmsep3  17411  cmpsub  17455  uncmp  17458  dfcon2  17474  cnconn  17477  1stcfb  17500  txuni2  17589  txbas  17591  ptbasin  17601  txcls  17628  txbasval  17630  txlly  17660  txnlly  17661  pthaus  17662  txlm  17672  tx1stc  17674  xkohaus  17677  isufil2  17932  ufileu  17943  cnpflfi  18023  txflf  18030  fclscf  18049  flimfnfcls  18052  alexsubb  18069  alexsubALTlem2  18071  alexsubALTlem4  18073  ptcmplem2  18076  ptcmplem3  18077  cnextcn  18090  divstgplem  18142  prdsmet  18392  blin2  18451  prdsbl  18513  nmolb  18743  tgqioo  18823  reconnlem2  18850  reconn  18851  lebnumlem3  18980  iscau4  19224  cmetcaulem  19233  iscmet3lem2  19237  bcthlem5  19273  minveclem3b  19321  pmltpc  19339  evthicc2  19349  ovolunlem2  19386  ovolicc2lem5  19409  mblsplit  19420  iundisj2  19435  volsup  19442  ioombl1lem4  19447  dyaddisj  19480  dyadmbllem  19483  i1faddlem  19577  itg10a  19594  itg1ge0a  19595  mbfi1flimlem  19606  mbfmullem  19609  itg2add  19643  rolle  19866  dvcvx  19896  itgsubst  19925  tdeglem4  19975  ply1domn  20038  fta1b  20084  plyadd  20128  plymul  20129  coeeu  20136  vieta1  20221  aalioulem6  20246  ulmcaulem  20302  ulmcau  20303  ulmbdd  20306  ulmcn  20307  amgm  20821  mumullem2  20955  ppiublem1  20978  dchrfi  21031  dchrptlem2  21041  dchrptlem3  21042  dchrsum2  21044  lgsdchr  21124  lgsquad2lem2  21135  2sqlem5  21144  2sqb  21154  pntlemp  21296  ostthlem2  21314  ostth  21325  usgra2edg  21394  nvmul0or  22125  ubthlem3  22366  axhcompl-zf  22493  hvmul0or  22519  ocnel  22792  pjhthmo  22796  spanuni  23038  spansni  23051  hon0  23288  leopadd  23627  leoptr  23632  mdsymlem6  23903  sumdmdlem2  23914  cdjreui  23927  iundisj2f  24022  iundisj2fi  24145  voliune  24577  volfiniune  24578  ballotlemimin  24755  txscon  24920  cvmsdisj  24949  cvmliftlem15  24977  cvmlift2lem10  24991  cvmlift3lem7  25004  prodmolem2  25253  prodmo  25254  dfon2lem3  25404  dfon2lem5  25406  dfon2lem6  25407  dfon2lem7  25408  dfon2lem8  25409  soseq  25521  frr3g  25573  nodenselem4  25631  nodenselem5  25632  nobndup  25647  nobnddown  25648  axcontlem8  25902  axcontlem9  25903  ifscgr  25970  cgr3tr4  25978  btwnconn1lem13  26025  seglecgr12  26037  ismblfin  26237  itg2addnclem3  26248  ftc1anclem6  26275  elicc3  26311  neibastop1  26379  tailfb  26397  fdc  26440  riscer  26595  intidl  26630  ispridlc  26671  prtlem14  26714  prtlem17  26716  diophin  26822  diophun  26823  psgneu  27397  pm10.57  27534  fnchoice  27667  swrdccatin1  28171  2cshwmod  28223  cshw1  28238  cshwssizelem1a  28242  bnj23  29020  bnj594  29220  bnj849  29233  ax10NEW7  29410  lpssat  29748  lssatle  29750  lshpkrlem6  29850  cvrnbtwn  30006  atlatmstc  30054  atlatle  30055  atlrelat1  30056  2at0mat0  30259  trlator0  30905  cdleme0moN  30959  cdlemn11pre  31945  dihord2pre  31960  dihmeetlem20N  32061  dochkrshp4  32124  lcfl6  32235
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 178
  Copyright terms: Public domain W3C validator