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

Theorem syl5bir 218
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 206 . 2  |-  ( ph  ->  ps )
3 syl5bir.2 . 2  |-  ( ch 
->  ( ps  ->  th )
)
42, 3syl5 32 1  |-  ( ch 
->  ( ph  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185
This theorem is referenced by:  3imtr3g  269  oplem1  948  nic-ax  1483  19.30  1658  19.33b  1662  hbnt  1826  necon4bd  2663  ssdisj  3716  pssdifn0  3728  disjss3  4279  somo  4662  frminex  4687  ordelord  4728  unizlim  4822  sofld  5274  funopfv  5719  mpteqb  5776  suppssrOLD  5825  funfvima  5939  fliftfun  5992  weniso  6032  tfinds  6459  tfindsg  6460  tfindes  6462  tfinds2  6463  findsg  6492  frxp  6671  suppssr  6709  rdgsucmptnf  6871  frsucmptn  6880  tz7.49  6886  om00  7002  oewordi  7018  iiner  7160  eroveu  7183  th3qlem1  7194  undom  7387  sdomdif  7447  php3  7485  sucdom2  7495  unxpdomlem3  7507  fisseneq  7512  pssnn  7519  ordunifi  7550  isfinite2  7558  fiint  7576  infssuni  7590  ixpfi2  7597  finsschain  7606  ordtypelem10  7729  wofib  7747  wemapsolem  7752  unxpwdom2  7791  sucprcregOLD  7803  inf3lem2  7823  cantnfp1lem3  7876  cantnfp1  7877  cantnfp1lem3OLD  7902  cantnfp1OLD  7903  setind  7942  r1tr  7971  r1ordg  7973  rankelb  8019  rankxplim3  8076  cardlim  8130  infxpenlem  8168  infxpenc2  8176  infxpenc2OLD  8180  dfac5lem4  8284  dfac12k  8304  kmlem13  8319  sornom  8434  fin23lem25  8481  fin23lem21  8496  zorn2lem4  8656  iundom2g  8692  fpwwe2lem12  8795  fpwwe2lem13  8796  pwfseqlem4a  8815  eltsk2g  8905  inttsk  8928  tskord  8934  r1tskina  8936  grudomon  8971  arch  10563  zaddcl  10672  uzm1  10878  xrsupsslem  11256  xrinfmsslem  11257  fsequb  11780  fseqsupubi  11783  seqf1o  11830  sq01  11969  swrdccatin1  12357  repsdf2  12399  cshw1  12439  rexanre  12817  rexuzre  12823  cau3lem  12825  o1co  13047  rlimcn2  13051  o1of2  13073  lo1add  13087  lo1mul  13088  climcau  13131  climbdd  13132  caucvgb  13140  summo  13177  isumltss  13293  mertenslem2  13327  bitsfzolem  13612  bitsfzo  13613  bezoutlem4  13707  prmind2  13756  isprm5  13780  pcqmul  13902  pcadd  13933  prmreclem2  13960  prmreclem5  13963  mul4sq  13997  vdwmc2  14022  ramcl  14072  prmlem1a  14116  divsfval  14467  iscatd2  14601  catpropd  14630  wunfunc  14791  gaorber  15805  psgneu  15991  lsmsubm  16131  pj1eu  16172  efgredlem  16223  divsabl  16326  cygabl  16346  cygctb  16347  lt6abl  16350  gsumval3eu  16360  dprdsubg  16494  ablfac1c  16545  pgpfac1  16554  dvdsrtr  16677  unitgrp  16692  drngmul0or  16776  lvecvs0or  17110  lspdisjb  17128  lspsolvlem  17144  lspprat  17155  lbsextlem2  17161  abvn0b  17295  domnchr  17804  znfld  17834  cygznlem3  17843  obselocv  17994  0ntr  18516  opnneiid  18571  restntr  18627  hausnei2  18798  nrmsep3  18800  cmpsub  18844  uncmp  18847  dfcon2  18864  cnconn  18867  1stcfb  18890  txuni2  18979  txbas  18981  ptbasin  18991  txcls  19018  txbasval  19020  txlly  19050  txnlly  19051  pthaus  19052  txlm  19062  tx1stc  19064  xkohaus  19067  isufil2  19322  ufileu  19333  cnpflfi  19413  txflf  19420  fclscf  19439  flimfnfcls  19442  alexsubb  19459  alexsubALTlem2  19461  alexsubALTlem4  19463  ptcmplem2  19466  ptcmplem3  19467  cnextcn  19480  divstgplem  19532  prdsmet  19786  blin2  19845  prdsbl  19907  nmolb  20137  tgqioo  20218  reconnlem2  20245  reconn  20246  lebnumlem3  20376  iscau4  20631  cmetcaulem  20640  iscmet3lem2  20644  bcthlem5  20680  minveclem3b  20756  pmltpc  20775  evthicc2  20785  ovolunlem2  20822  ovolicc2lem5  20845  mblsplit  20856  iundisj2  20871  volsup  20878  ioombl1lem4  20883  dyaddisj  20917  dyadmbllem  20920  i1faddlem  21012  itg10a  21029  itg1ge0a  21030  mbfi1flimlem  21041  mbfmullem  21044  itg2add  21078  rolle  21303  dvcvx  21333  itgsubst  21362  tdeglem4  21413  ply1domn  21479  fta1b  21525  plyadd  21569  plymul  21570  coeeu  21577  vieta1  21662  aalioulem6  21687  ulmcaulem  21743  ulmcau  21744  ulmbdd  21747  ulmcn  21748  amgm  22268  mumullem2  22402  ppiublem1  22425  dchrfi  22478  dchrptlem2  22488  dchrptlem3  22489  dchrsum2  22491  lgsdchr  22571  lgsquad2lem2  22582  2sqlem5  22591  2sqb  22601  pntlemp  22743  ostthlem2  22761  ostth  22772  tgbtwnconn1  22882  colline  22917  axcontlem8  23039  axcontlem9  23040  usgra2edg  23123  nvmul0or  23854  ubthlem3  24095  axhcompl-zf  24222  hvmul0or  24249  ocnel  24523  pjhthmo  24527  spanuni  24769  spansni  24782  hon0  25019  leopadd  25358  leoptr  25363  mdsymlem6  25634  sumdmdlem2  25645  cdjreui  25658  spc2d  25680  iundisj2f  25755  disjunsn  25759  iundisj2fi  25903  voliune  26498  volfiniune  26499  ballotlemimin  26735  txscon  26977  cvmsdisj  27006  cvmliftlem15  27034  cvmlift2lem10  27048  cvmlift3lem7  27061  prodmolem2  27294  prodmo  27295  dfon2lem3  27444  dfon2lem5  27446  dfon2lem6  27447  dfon2lem7  27448  dfon2lem8  27449  soseq  27561  frr3g  27613  nodenselem4  27671  nodenselem5  27672  nobndup  27687  nobnddown  27688  ifscgr  27921  cgr3tr4  27929  btwnconn1lem13  27976  seglecgr12  27988  wl-equsal1i  28218  ismblfin  28273  itg2addnclem3  28286  ftc1anclem6  28313  elicc3  28353  neibastop1  28421  tailfb  28439  fdc  28482  riscer  28635  intidl  28670  ispridlc  28711  prtlem14  28861  prtlem17  28863  diophin  28953  diophun  28954  pm10.57  29465  fnchoice  29593  ralnralall  29961  f0rn0  29984  fvelrnfvelrnressn  29994  2ffzoeq  30057  usg2wlkeq  30132  clwlkisclwwlklem2a4  30289  clwwisshclwwn  30315  frgraregord013  30554  snlindsntor  30711  islininds2  30724  bnj23  31406  bnj594  31604  bnj849  31617  bj-sngltag  32056  lpssat  32228  lssatle  32230  lshpkrlem6  32330  cvrnbtwn  32486  atlatmstc  32534  atlatle  32535  atlrelat1  32536  2at0mat0  32739  trlator0  33385  cdleme0moN  33439  cdlemn11pre  34425  dihord2pre  34440  dihmeetlem20N  34541  dochkrshp4  34604  lcfl6  34715
  Copyright terms: Public domain W3C validator