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

Theorem syl5bir 226
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 211 . 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 189
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 190
This theorem is referenced by:  3imtr3g  277  oplem1  976  nic-ax  1564  19.30  1752  19.33b  1756  hbnt  1996  necon1bd  2661  pssdifn0  3743  ssdisj  3818  disjss3  4394  somo  4794  frminex  4819  sofld  5290  ordelord  5452  unizlim  5546  f0rn0  5781  funopfv  5918  mpteqb  5979  fvrnressn  6095  funfvima  6157  fliftfun  6223  weniso  6263  tfinds  6705  tfindsg  6706  tfindes  6708  tfinds2  6709  findsg  6739  frxp  6925  suppssr  6965  rdgsucmptnf  7165  frsucmptn  7174  tz7.49  7180  om00  7294  oewordi  7310  iiner  7453  eroveu  7476  undom  7678  sdomdif  7738  php3  7776  sucdom2  7786  unxpdomlem3  7796  fisseneq  7801  pssnn  7808  ordunifi  7839  isfinite2  7847  fiint  7866  infssuni  7883  ixpfi2  7890  finsschain  7899  ordtypelem10  8060  wofib  8078  wemapsolem  8083  unxpwdom2  8121  inf3lem2  8152  cantnfp1lem3  8203  cantnfp1  8204  setind  8236  r1tr  8265  r1ordg  8267  rankelb  8313  rankxplim3  8370  cardlim  8424  infxpenlem  8462  infxpenc2  8471  dfac5lem4  8575  dfac12k  8595  kmlem13  8610  sornom  8725  fin23lem25  8772  fin23lem21  8787  zorn2lem4  8947  iundom2g  8983  fpwwe2lem12  9084  fpwwe2lem13  9085  pwfseqlem4a  9104  eltsk2g  9194  inttsk  9217  tskord  9223  r1tskina  9225  grudomon  9260  arch  10890  zaddcl  11001  uzm1  11213  xrsupsslem  11617  xrinfmsslem  11618  fsequb  12226  fseqsupubi  12229  ssnn0fi  12235  seqf1o  12292  sq01  12432  ccatalpha  12787  swrdccatin1  12893  repsdf2  12935  cshw1  12978  rexanre  13486  rexuzre  13492  cau3lem  13494  o1co  13727  rlimcn2  13731  o1of2  13753  lo1add  13767  lo1mul  13768  climcau  13811  climbdd  13812  caucvgb  13823  summo  13860  isumltss  13983  mertenslem2  14018  prodmolem2  14066  prodmo  14067  bitsfzolem  14486  bitsfzolemOLD  14487  bitsfzo  14488  bezoutlem4OLD  14585  bezoutlem4  14588  lcmfeq0b  14682  lcmfunsnlem2  14692  prmind2  14714  isprm5  14730  pcqmul  14882  pcadd  14913  prmreclem2  14940  prmreclem5  14943  mul4sq  14977  vdwmc2  15008  ramcl  15066  prmgaplem7  15106  prmlem1a  15156  divsfval  15531  iscatd2  15665  catpropd  15692  wunfunc  15882  gaorber  17040  psgneu  17225  lsmsubm  17383  pj1eu  17424  efgredlem  17475  qusabl  17581  cygabl  17603  cygctb  17604  lt6abl  17607  gsumval3eu  17616  dprdsubg  17735  ablfac1c  17782  pgpfac1  17791  dvdsrtr  17958  unitgrp  17973  drngmul0or  18074  lvecvs0or  18409  lspdisjb  18427  lspsolvlem  18443  lspprat  18454  lbsextlem2  18460  abvn0b  18603  domnchr  19180  znfld  19208  cygznlem3  19217  obselocv  19368  cpmatacl  19817  chfacfisf  19955  chfacfisfcpmat  19956  0ntr  20164  opnneiid  20219  restntr  20275  hausnei2  20446  nrmsep3  20448  cmpsub  20492  uncmp  20495  dfcon2  20511  cnconn  20514  1stcfb  20537  txuni2  20657  txbas  20659  ptbasin  20669  txcls  20696  txbasval  20698  txlly  20728  txnlly  20729  pthaus  20730  txlm  20740  tx1stc  20742  xkohaus  20745  isufil2  21001  ufileu  21012  cnpflfi  21092  txflf  21099  fclscf  21118  flimfnfcls  21121  alexsubb  21139  alexsubALTlem2  21141  alexsubALTlem4  21143  ptcmplem2  21146  ptcmplem3  21147  cnextcn  21160  qustgplem  21213  prdsmet  21463  blin2  21522  prdsbl  21584  nmolb  21800  nmolbOLD  21819  tgqioo  21896  reconnlem2  21923  reconn  21924  lebnumlem3  22069  lebnumlem3OLD  22072  iscau4  22327  cmetcaulem  22336  iscmet3lem2  22340  bcthlem5  22374  minveclem3b  22448  minveclem3bOLD  22460  pmltpc  22479  evthicc2  22489  ovolunlem2  22529  ovolicc2lem5  22553  mblsplit  22564  iundisj2  22581  volsup  22588  ioombl1lem4  22593  dyaddisj  22633  dyadmbllem  22636  i1faddlem  22730  itg10a  22747  itg1ge0a  22748  mbfi1flimlem  22759  mbfmullem  22762  itg2add  22796  rolle  23021  dvcvx  23051  itgsubst  23080  tdeglem4  23088  ply1domn  23151  fta1b  23199  plyadd  23250  plymul  23251  coeeu  23258  vieta1  23344  aalioulem6  23372  ulmcaulem  23428  ulmcau  23429  ulmbdd  23432  ulmcn  23433  amgm  23995  mumullem2  24186  ppiublem1  24209  dchrfi  24262  dchrptlem2  24272  dchrptlem3  24273  dchrsum2  24275  lgsdchr  24355  lgsquad2lem2  24366  2sqlem5  24375  2sqb  24385  pntlemp  24527  ostthlem2  24545  ostth  24556  iscgrglt  24638  tgbtwnconn1  24699  colline  24773  lmimid  24915  axcontlem8  25080  axcontlem9  25081  eengtrkg  25094  usgra2edg  25188  usg2wlkeq  25515  clwlkisclwwlklem2a4  25591  clwwisshclwwn  25615  frgraregord013  25925  nvmul0or  26354  ubthlem3  26595  axhcompl-zf  26732  hvmul0or  26759  ocnel  27032  pjhthmo  27036  spanuni  27278  spansni  27291  hon0  27527  leopadd  27866  leoptr  27871  mdsymlem6  28142  sumdmdlem2  28153  cdjreui  28166  spc2d  28188  iundisj2f  28277  disjunsn  28281  iundisj2fi  28448  ballotlemimin  29411  ballotlemiminOLD  29449  bnj23  29596  bnj594  29795  bnj849  29808  txscon  30036  cvmsdisj  30065  cvmliftlem15  30093  cvmlift2lem10  30107  cvmlift3lem7  30120  mclsppslem  30293  dfon2lem3  30502  dfon2lem5  30504  dfon2lem6  30505  dfon2lem7  30506  dfon2lem8  30507  soseq  30563  frr3g  30584  nodenselem4  30644  nodenselem5  30645  nobndup  30660  nobnddown  30661  ifscgr  30882  cgr3tr4  30890  btwnconn1lem13  30937  seglecgr12  30949  elicc3  31044  neibastop1  31086  tailfb  31104  bj-sngltag  31647  bj-elid  31710  mptsnunlem  31810  finxpreclem6  31858  wl-equsal1i  31946  poimirlem26  32030  poimirlem27  32031  ismblfin  32045  itg2addnclem3  32059  ftc1anclem6  32086  fdc  32138  riscer  32291  intidl  32326  ispridlc  32367  prtlem14  32510  prtlem17  32512  lpssat  32650  lssatle  32652  lshpkrlem6  32752  cvrnbtwn  32908  atlatmstc  32956  atlatle  32957  atlrelat1  32958  2at0mat0  33161  trlator0  33808  cdleme0moN  33862  cdlemn11pre  34849  dihord2pre  34864  dihmeetlem20N  34965  dochkrshp4  35028  lcfl6  35139  diophin  35686  diophun  35687  pm10.57  36790  fnchoice  37413  ellimcabssub0  37794  fourierdlem81  38163  fourierdlem93  38175  fzopredsuc  38865  iccpartlt  38883  bgoldbst  39024  nnsum4primesevenALTV  39041  cshword2  39125  ralnralall  39132  fpropnf1  39182  2ffzoeq  39209  structgrssvtxlem  39278  uhgr2edg  39453  1wlkdlem2  39883  spthdep  39926  pthdlem2  39954  nzerooringczr  40582  ply1mulgsumlem1  40686  snlindsntor  40772  islininds2  40785  m1modmmod  40832
  Copyright terms: Public domain W3C validator