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

Theorem syl5bir 222
Description: A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 21-Jun-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 210 . 2  |-  ( ph  ->  ps )
3 syl5bir.2 . 2  |-  ( ch 
->  ( ps  ->  th )
)
42, 3syl5 34 1  |-  ( ch 
->  ( ph  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188
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 189
This theorem is referenced by:  3imtr3g  273  oplem1  973  nic-ax  1553  19.30  1737  19.33b  1741  hbnt  1950  necon1bd  2643  necon4bdOLD  2648  ssdisj  3843  pssdifn0  3856  disjss3  4420  somo  4806  frminex  4831  sofld  5301  ordelord  5462  unizlim  5556  f0rn0  5783  funopfv  5918  mpteqb  5978  fvrnressn  6092  funfvima  6153  fliftfun  6218  weniso  6258  tfinds  6698  tfindsg  6699  tfindes  6701  tfinds2  6702  findsg  6732  frxp  6915  suppssr  6955  rdgsucmptnf  7153  frsucmptn  7162  tz7.49  7168  om00  7282  oewordi  7298  iiner  7441  eroveu  7464  undom  7664  sdomdif  7724  php3  7762  sucdom2  7772  unxpdomlem3  7782  fisseneq  7787  pssnn  7794  ordunifi  7825  isfinite2  7833  fiint  7852  infssuni  7869  ixpfi2  7876  finsschain  7885  ordtypelem10  8046  wofib  8064  wemapsolem  8069  unxpwdom2  8107  inf3lem2  8138  cantnfp1lem3  8188  cantnfp1  8189  setind  8221  r1tr  8250  r1ordg  8252  rankelb  8298  rankxplim3  8355  cardlim  8409  infxpenlem  8447  infxpenc2  8455  dfac5lem4  8559  dfac12k  8579  kmlem13  8594  sornom  8709  fin23lem25  8756  fin23lem21  8771  zorn2lem4  8931  iundom2g  8967  fpwwe2lem12  9068  fpwwe2lem13  9069  pwfseqlem4a  9088  eltsk2g  9178  inttsk  9201  tskord  9207  r1tskina  9209  grudomon  9244  arch  10868  zaddcl  10979  uzm1  11191  xrsupsslem  11594  xrinfmsslem  11595  fsequb  12189  fseqsupubi  12192  ssnn0fi  12198  seqf1o  12255  sq01  12395  swrdccatin1  12835  repsdf2  12877  cshw1  12917  rexanre  13403  rexuzre  13409  cau3lem  13411  o1co  13643  rlimcn2  13647  o1of2  13669  lo1add  13683  lo1mul  13684  climcau  13727  climbdd  13728  caucvgb  13739  summo  13776  isumltss  13899  mertenslem2  13934  prodmolem2  13982  prodmo  13983  bitsfzolem  14400  bitsfzolemOLD  14401  bitsfzo  14402  bezoutlem4OLD  14499  bezoutlem4  14502  lcmfeq0b  14596  lcmfunsnlem2  14606  prmind2  14628  isprm5  14644  pcqmul  14796  pcadd  14827  prmreclem2  14854  prmreclem5  14857  mul4sq  14891  vdwmc2  14922  ramcl  14980  prmgaplem7  15020  prmlem1a  15071  divsfval  15446  iscatd2  15580  catpropd  15607  wunfunc  15797  gaorber  16955  psgneu  17140  lsmsubm  17298  pj1eu  17339  efgredlem  17390  qusabl  17496  cygabl  17518  cygctb  17519  lt6abl  17522  gsumval3eu  17531  dprdsubg  17650  ablfac1c  17697  pgpfac1  17706  dvdsrtr  17873  unitgrp  17888  drngmul0or  17989  lvecvs0or  18324  lspdisjb  18342  lspsolvlem  18358  lspprat  18369  lbsextlem2  18375  abvn0b  18519  domnchr  19095  znfld  19123  cygznlem3  19132  obselocv  19283  cpmatacl  19732  chfacfisf  19870  chfacfisfcpmat  19871  0ntr  20079  opnneiid  20134  restntr  20190  hausnei2  20361  nrmsep3  20363  cmpsub  20407  uncmp  20410  dfcon2  20426  cnconn  20429  1stcfb  20452  txuni2  20572  txbas  20574  ptbasin  20584  txcls  20611  txbasval  20613  txlly  20643  txnlly  20644  pthaus  20645  txlm  20655  tx1stc  20657  xkohaus  20660  isufil2  20915  ufileu  20926  cnpflfi  21006  txflf  21013  fclscf  21032  flimfnfcls  21035  alexsubb  21053  alexsubALTlem2  21055  alexsubALTlem4  21057  ptcmplem2  21060  ptcmplem3  21061  cnextcn  21074  qustgplem  21127  prdsmet  21377  blin2  21436  prdsbl  21498  nmolb  21714  nmolbOLD  21733  tgqioo  21810  reconnlem2  21837  reconn  21838  lebnumlem3  21983  lebnumlem3OLD  21986  iscau4  22241  cmetcaulem  22250  iscmet3lem2  22254  bcthlem5  22288  minveclem3b  22362  minveclem3bOLD  22374  pmltpc  22393  evthicc2  22403  ovolunlem2  22443  ovolicc2lem5  22467  mblsplit  22478  iundisj2  22494  volsup  22501  ioombl1lem4  22506  dyaddisj  22546  dyadmbllem  22549  i1faddlem  22643  itg10a  22660  itg1ge0a  22661  mbfi1flimlem  22672  mbfmullem  22675  itg2add  22709  rolle  22934  dvcvx  22964  itgsubst  22993  tdeglem4  23001  ply1domn  23064  fta1b  23112  plyadd  23163  plymul  23164  coeeu  23171  vieta1  23257  aalioulem6  23285  ulmcaulem  23341  ulmcau  23342  ulmbdd  23345  ulmcn  23346  amgm  23908  mumullem2  24099  ppiublem1  24122  dchrfi  24175  dchrptlem2  24185  dchrptlem3  24186  dchrsum2  24188  lgsdchr  24268  lgsquad2lem2  24279  2sqlem5  24288  2sqb  24298  pntlemp  24440  ostthlem2  24458  ostth  24469  iscgrglt  24551  tgbtwnconn1  24612  colline  24686  lmimid  24828  axcontlem8  24993  axcontlem9  24994  eengtrkg  25007  usgra2edg  25101  usg2wlkeq  25428  clwlkisclwwlklem2a4  25504  clwwisshclwwn  25528  frgraregord013  25838  nvmul0or  26265  ubthlem3  26506  axhcompl-zf  26643  hvmul0or  26670  ocnel  26943  pjhthmo  26947  spanuni  27189  spansni  27202  hon0  27438  leopadd  27777  leoptr  27782  mdsymlem6  28053  sumdmdlem2  28064  cdjreui  28077  spc2d  28099  iundisj2f  28196  disjunsn  28200  iundisj2fi  28373  ballotlemimin  29340  ballotlemiminOLD  29378  bnj23  29526  bnj594  29725  bnj849  29738  txscon  29966  cvmsdisj  29995  cvmliftlem15  30023  cvmlift2lem10  30037  cvmlift3lem7  30050  mclsppslem  30223  dfon2lem3  30432  dfon2lem5  30434  dfon2lem6  30435  dfon2lem7  30436  dfon2lem8  30437  soseq  30493  frr3g  30514  nodenselem4  30572  nodenselem5  30573  nobndup  30588  nobnddown  30589  ifscgr  30810  cgr3tr4  30818  btwnconn1lem13  30865  seglecgr12  30877  elicc3  30972  neibastop1  31014  tailfb  31032  bj-sngltag  31539  bj-elid  31597  mptsnunlem  31687  wl-equsal1i  31796  poimirlem26  31886  poimirlem27  31887  ismblfin  31901  itg2addnclem3  31915  ftc1anclem6  31942  fdc  31994  riscer  32147  intidl  32182  ispridlc  32223  prtlem14  32370  prtlem17  32372  lpssat  32504  lssatle  32506  lshpkrlem6  32606  cvrnbtwn  32762  atlatmstc  32810  atlatle  32811  atlrelat1  32812  2at0mat0  33015  trlator0  33662  cdleme0moN  33716  cdlemn11pre  34703  dihord2pre  34718  dihmeetlem20N  34819  dochkrshp4  34882  lcfl6  34993  diophin  35540  diophun  35541  pm10.57  36584  fnchoice  37217  ellimcabssub0  37523  fourierdlem81  37877  fourierdlem93  37889  fzopredsuc  38438  iccpartlt  38456  bgoldbst  38597  nnsum4primesevenALTV  38614  cshword2  38696  ralnralall  38699  2ffzoeq  38759  struct1vtxvallem  38795  usgr2edg  38916  nzerooringczr  39378  ply1mulgsumlem1  39484  snlindsntor  39570  islininds2  39583  m1modmmod  39630
  Copyright terms: Public domain W3C validator