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, 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 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  955  nic-ax  1480  19.30  1659  19.33b  1663  hbnt  1828  necon4bd  2697  ssdisj  3749  pssdifn0  3761  disjss3  4312  somo  4696  frminex  4721  ordelord  4762  unizlim  4856  sofld  5307  funopfv  5752  mpteqb  5809  suppssrOLD  5858  funfvima  5973  fliftfun  6026  weniso  6066  tfinds  6491  tfindsg  6492  tfindes  6494  tfinds2  6495  findsg  6524  frxp  6703  suppssr  6741  rdgsucmptnf  6906  frsucmptn  6915  tz7.49  6921  om00  7035  oewordi  7051  iiner  7193  eroveu  7216  th3qlem1  7227  undom  7420  sdomdif  7480  php3  7518  sucdom2  7528  unxpdomlem3  7540  fisseneq  7545  pssnn  7552  ordunifi  7583  isfinite2  7591  fiint  7609  infssuni  7623  ixpfi2  7630  finsschain  7639  ordtypelem10  7762  wofib  7780  wemapsolem  7785  unxpwdom2  7824  sucprcregOLD  7836  inf3lem2  7856  cantnfp1lem3  7909  cantnfp1  7910  cantnfp1lem3OLD  7935  cantnfp1OLD  7936  setind  7975  r1tr  8004  r1ordg  8006  rankelb  8052  rankxplim3  8109  cardlim  8163  infxpenlem  8201  infxpenc2  8209  infxpenc2OLD  8213  dfac5lem4  8317  dfac12k  8337  kmlem13  8352  sornom  8467  fin23lem25  8514  fin23lem21  8529  zorn2lem4  8689  iundom2g  8725  fpwwe2lem12  8829  fpwwe2lem13  8830  pwfseqlem4a  8849  eltsk2g  8939  inttsk  8962  tskord  8968  r1tskina  8970  grudomon  9005  arch  10597  zaddcl  10706  uzm1  10912  xrsupsslem  11290  xrinfmsslem  11291  fsequb  11818  fseqsupubi  11821  seqf1o  11868  sq01  12007  swrdccatin1  12395  repsdf2  12437  cshw1  12477  rexanre  12855  rexuzre  12861  cau3lem  12863  o1co  13085  rlimcn2  13089  o1of2  13111  lo1add  13125  lo1mul  13126  climcau  13169  climbdd  13170  caucvgb  13178  summo  13215  isumltss  13332  mertenslem2  13366  bitsfzolem  13651  bitsfzo  13652  bezoutlem4  13746  prmind2  13795  isprm5  13819  pcqmul  13941  pcadd  13972  prmreclem2  13999  prmreclem5  14002  mul4sq  14036  vdwmc2  14061  ramcl  14111  prmlem1a  14155  divsfval  14506  iscatd2  14640  catpropd  14669  wunfunc  14830  gaorber  15847  psgneu  16033  lsmsubm  16173  pj1eu  16214  efgredlem  16265  divsabl  16368  cygabl  16388  cygctb  16389  lt6abl  16392  gsumval3eu  16402  dprdsubg  16543  ablfac1c  16594  pgpfac1  16603  dvdsrtr  16766  unitgrp  16781  drngmul0or  16875  lvecvs0or  17211  lspdisjb  17229  lspsolvlem  17245  lspprat  17256  lbsextlem2  17262  abvn0b  17396  domnchr  17985  znfld  18015  cygznlem3  18024  obselocv  18175  0ntr  18697  opnneiid  18752  restntr  18808  hausnei2  18979  nrmsep3  18981  cmpsub  19025  uncmp  19028  dfcon2  19045  cnconn  19048  1stcfb  19071  txuni2  19160  txbas  19162  ptbasin  19172  txcls  19199  txbasval  19201  txlly  19231  txnlly  19232  pthaus  19233  txlm  19243  tx1stc  19245  xkohaus  19248  isufil2  19503  ufileu  19514  cnpflfi  19594  txflf  19601  fclscf  19620  flimfnfcls  19623  alexsubb  19640  alexsubALTlem2  19642  alexsubALTlem4  19644  ptcmplem2  19647  ptcmplem3  19648  cnextcn  19661  divstgplem  19713  prdsmet  19967  blin2  20026  prdsbl  20088  nmolb  20318  tgqioo  20399  reconnlem2  20426  reconn  20427  lebnumlem3  20557  iscau4  20812  cmetcaulem  20821  iscmet3lem2  20825  bcthlem5  20861  minveclem3b  20937  pmltpc  20956  evthicc2  20966  ovolunlem2  21003  ovolicc2lem5  21026  mblsplit  21037  iundisj2  21052  volsup  21059  ioombl1lem4  21064  dyaddisj  21098  dyadmbllem  21101  i1faddlem  21193  itg10a  21210  itg1ge0a  21211  mbfi1flimlem  21222  mbfmullem  21225  itg2add  21259  rolle  21484  dvcvx  21514  itgsubst  21543  tdeglem4  21551  ply1domn  21617  fta1b  21663  plyadd  21707  plymul  21708  coeeu  21715  vieta1  21800  aalioulem6  21825  ulmcaulem  21881  ulmcau  21882  ulmbdd  21885  ulmcn  21886  amgm  22406  mumullem2  22540  ppiublem1  22563  dchrfi  22616  dchrptlem2  22626  dchrptlem3  22627  dchrsum2  22629  lgsdchr  22709  lgsquad2lem2  22720  2sqlem5  22729  2sqb  22739  pntlemp  22881  ostthlem2  22899  ostth  22910  tgbtwnconn1  23029  colline  23074  axcontlem8  23239  axcontlem9  23240  usgra2edg  23323  nvmul0or  24054  ubthlem3  24295  axhcompl-zf  24422  hvmul0or  24449  ocnel  24723  pjhthmo  24727  spanuni  24969  spansni  24982  hon0  25219  leopadd  25558  leoptr  25563  mdsymlem6  25834  sumdmdlem2  25845  cdjreui  25858  spc2d  25880  iundisj2f  25954  disjunsn  25958  iundisj2fi  26103  voliune  26667  volfiniune  26668  ballotlemimin  26910  txscon  27152  cvmsdisj  27181  cvmliftlem15  27209  cvmlift2lem10  27223  cvmlift3lem7  27236  prodmolem2  27470  prodmo  27471  dfon2lem3  27620  dfon2lem5  27622  dfon2lem6  27623  dfon2lem7  27624  dfon2lem8  27625  soseq  27737  frr3g  27789  nodenselem4  27847  nodenselem5  27848  nobndup  27863  nobnddown  27864  ifscgr  28097  cgr3tr4  28105  btwnconn1lem13  28152  seglecgr12  28164  wl-equsal1i  28398  ismblfin  28458  itg2addnclem3  28471  ftc1anclem6  28498  elicc3  28538  neibastop1  28606  tailfb  28624  fdc  28667  riscer  28820  intidl  28855  ispridlc  28896  prtlem14  29045  prtlem17  29047  diophin  29137  diophun  29138  pm10.57  29649  fnchoice  29777  ralnralall  30144  f0rn0  30167  fvelrnfvelrnressn  30177  2ffzoeq  30240  usg2wlkeq  30315  clwlkisclwwlklem2a4  30472  clwwisshclwwn  30498  frgraregord013  30737  ssnn0fi  30775  ply1mulgsumlem1  30877  scmatsubcl  30923  scmatmulcl  30925  snlindsntor  31002  islininds2  31015  cnstpmatacl  31068  bnj23  31803  bnj594  32001  bnj849  32014  bj-sngltag  32572  lpssat  32754  lssatle  32756  lshpkrlem6  32856  cvrnbtwn  33012  atlatmstc  33060  atlatle  33061  atlrelat1  33062  2at0mat0  33265  trlator0  33911  cdleme0moN  33965  cdlemn11pre  34951  dihord2pre  34966  dihmeetlem20N  35067  dochkrshp4  35130  lcfl6  35241
  Copyright terms: Public domain W3C validator