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  962  nic-ax  1490  19.30  1669  19.33b  1673  hbnt  1842  necon1bd  2685  necon4bdOLD  2690  ssdisj  3876  pssdifn0  3888  disjss3  4446  somo  4834  frminex  4859  ordelord  4900  unizlim  4994  sofld  5455  f0rn0  5770  funopfv  5907  mpteqb  5964  suppssrOLD  6015  fvrnressn  6076  funfvima  6135  fliftfun  6198  weniso  6238  tfinds  6678  tfindsg  6679  tfindes  6681  tfinds2  6682  findsg  6711  frxp  6893  suppssr  6931  rdgsucmptnf  7095  frsucmptn  7104  tz7.49  7110  om00  7224  oewordi  7240  iiner  7383  eroveu  7406  undom  7605  sdomdif  7665  php3  7703  sucdom2  7714  unxpdomlem3  7726  fisseneq  7731  pssnn  7738  ordunifi  7770  isfinite2  7778  fiint  7797  infssuni  7811  ixpfi2  7818  finsschain  7827  ordtypelem10  7952  wofib  7970  wemapsolem  7975  unxpwdom2  8014  sucprcregOLD  8026  inf3lem2  8046  cantnfp1lem3  8099  cantnfp1  8100  cantnfp1lem3OLD  8125  cantnfp1OLD  8126  setind  8165  r1tr  8194  r1ordg  8196  rankelb  8242  rankxplim3  8299  cardlim  8353  infxpenlem  8391  infxpenc2  8399  infxpenc2OLD  8403  dfac5lem4  8507  dfac12k  8527  kmlem13  8542  sornom  8657  fin23lem25  8704  fin23lem21  8719  zorn2lem4  8879  iundom2g  8915  fpwwe2lem12  9019  fpwwe2lem13  9020  pwfseqlem4a  9039  eltsk2g  9129  inttsk  9152  tskord  9158  r1tskina  9160  grudomon  9195  arch  10792  zaddcl  10903  uzm1  11112  xrsupsslem  11498  xrinfmsslem  11499  fsequb  12053  fseqsupubi  12056  ssnn0fi  12062  seqf1o  12116  sq01  12256  swrdccatin1  12671  repsdf2  12713  cshw1  12753  rexanre  13142  rexuzre  13148  cau3lem  13150  o1co  13372  rlimcn2  13376  o1of2  13398  lo1add  13412  lo1mul  13413  climcau  13456  climbdd  13457  caucvgb  13465  summo  13502  isumltss  13623  mertenslem2  13657  bitsfzolem  13943  bitsfzo  13944  bezoutlem4  14038  prmind2  14087  isprm5  14112  pcqmul  14236  pcadd  14267  prmreclem2  14294  prmreclem5  14297  mul4sq  14331  vdwmc2  14356  ramcl  14406  prmlem1a  14450  divsfval  14802  iscatd2  14936  catpropd  14965  wunfunc  15126  gaorber  16151  psgneu  16337  lsmsubm  16479  pj1eu  16520  efgredlem  16571  divsabl  16674  cygabl  16696  cygctb  16697  lt6abl  16700  gsumval3eu  16710  dprdsubg  16873  ablfac1c  16924  pgpfac1  16933  dvdsrtr  17102  unitgrp  17117  drngmul0or  17217  lvecvs0or  17554  lspdisjb  17572  lspsolvlem  17588  lspprat  17599  lbsextlem2  17605  abvn0b  17750  domnchr  18364  znfld  18394  cygznlem3  18403  obselocv  18554  cpmatacl  19012  chfacfisf  19150  chfacfisfcpmat  19151  0ntr  19366  opnneiid  19421  restntr  19477  hausnei2  19648  nrmsep3  19650  cmpsub  19694  uncmp  19697  dfcon2  19714  cnconn  19717  1stcfb  19740  txuni2  19829  txbas  19831  ptbasin  19841  txcls  19868  txbasval  19870  txlly  19900  txnlly  19901  pthaus  19902  txlm  19912  tx1stc  19914  xkohaus  19917  isufil2  20172  ufileu  20183  cnpflfi  20263  txflf  20270  fclscf  20289  flimfnfcls  20292  alexsubb  20309  alexsubALTlem2  20311  alexsubALTlem4  20313  ptcmplem2  20316  ptcmplem3  20317  cnextcn  20330  divstgplem  20382  prdsmet  20636  blin2  20695  prdsbl  20757  nmolb  20987  tgqioo  21068  reconnlem2  21095  reconn  21096  lebnumlem3  21226  iscau4  21481  cmetcaulem  21490  iscmet3lem2  21494  bcthlem5  21530  minveclem3b  21606  pmltpc  21625  evthicc2  21635  ovolunlem2  21672  ovolicc2lem5  21695  mblsplit  21706  iundisj2  21722  volsup  21729  ioombl1lem4  21734  dyaddisj  21768  dyadmbllem  21771  i1faddlem  21863  itg10a  21880  itg1ge0a  21881  mbfi1flimlem  21892  mbfmullem  21895  itg2add  21929  rolle  22154  dvcvx  22184  itgsubst  22213  tdeglem4  22221  ply1domn  22287  fta1b  22333  plyadd  22377  plymul  22378  coeeu  22385  vieta1  22470  aalioulem6  22495  ulmcaulem  22551  ulmcau  22552  ulmbdd  22555  ulmcn  22556  amgm  23076  mumullem2  23210  ppiublem1  23233  dchrfi  23286  dchrptlem2  23296  dchrptlem3  23297  dchrsum2  23299  lgsdchr  23379  lgsquad2lem2  23390  2sqlem5  23399  2sqb  23409  pntlemp  23551  ostthlem2  23569  ostth  23580  tgbtwnconn1  23717  colline  23771  lmimid  23864  axcontlem8  23978  axcontlem9  23979  usgra2edg  24086  usg2wlkeq  24412  clwlkisclwwlklem2a4  24488  clwwisshclwwn  24512  frgraregord013  24823  nvmul0or  25251  ubthlem3  25492  axhcompl-zf  25619  hvmul0or  25646  ocnel  25920  pjhthmo  25924  spanuni  26166  spansni  26179  hon0  26416  leopadd  26755  leoptr  26760  mdsymlem6  27031  sumdmdlem2  27042  cdjreui  27055  spc2d  27077  iundisj2f  27150  disjunsn  27154  iundisj2fi  27298  voliune  27869  volfiniune  27870  ballotlemimin  28112  txscon  28354  cvmsdisj  28383  cvmliftlem15  28411  cvmlift2lem10  28425  cvmlift3lem7  28438  prodmolem2  28672  prodmo  28673  dfon2lem3  28822  dfon2lem5  28824  dfon2lem6  28825  dfon2lem7  28826  dfon2lem8  28827  soseq  28939  frr3g  28991  nodenselem4  29049  nodenselem5  29050  nobndup  29065  nobnddown  29066  ifscgr  29299  cgr3tr4  29307  btwnconn1lem13  29354  seglecgr12  29366  wl-equsal1i  29601  ismblfin  29660  itg2addnclem3  29673  ftc1anclem6  29700  elicc3  29740  neibastop1  29808  tailfb  29826  fdc  29869  riscer  30022  intidl  30057  ispridlc  30098  prtlem14  30247  prtlem17  30249  diophin  30338  diophun  30339  pm10.57  30882  fnchoice  31010  fourierdlem93  31528  ralnralall  31789  2ffzoeq  31836  ply1mulgsumlem1  32085  snlindsntor  32171  islininds2  32184  bnj23  32869  bnj594  33067  bnj849  33080  bj-sngltag  33640  bj-elid  33690  lpssat  33828  lssatle  33830  lshpkrlem6  33930  cvrnbtwn  34086  atlatmstc  34134  atlatle  34135  atlrelat1  34136  2at0mat0  34339  trlator0  34985  cdleme0moN  35039  cdlemn11pre  36025  dihord2pre  36040  dihmeetlem20N  36141  dochkrshp4  36204  lcfl6  36315
  Copyright terms: Public domain W3C validator