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

Theorem syl5bir 210
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 198 . 2  |-  ( ph  ->  ps )
3 syl5bir.2 . 2  |-  ( ch 
->  ( ps  ->  th )
)
42, 3syl5 30 1  |-  ( ch 
->  ( ph  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  3imtr3g  261  oplem1  931  nic-ax  1444  19.30  1611  19.33b  1615  ax10OLD  1988  necon4bd  2612  ceqex  3009  ssdisj  3620  pssdifn0  3632  disjss3  4152  somo  4478  frminex  4503  ordelord  4544  unizlim  4638  tfinds  4779  tfindsg  4780  tfindes  4782  tfinds2  4783  findsg  4812  sofld  5258  funopfv  5705  mpteqb  5758  suppssr  5803  funfvima  5912  fliftfun  5973  weniso  6014  frxp  6392  rdgsucmptnf  6623  frsucmptn  6632  tz7.49  6638  om00  6754  oewordi  6770  iiner  6912  eroveu  6935  th3qlem1  6946  undom  7132  sdomdif  7191  php3  7229  sucdom2  7239  unxpdomlem3  7251  fisseneq  7256  pssnn  7263  ordunifi  7293  isfinite2  7301  fiint  7319  ixpfi2  7340  finsschain  7348  ordtypelem10  7429  wofib  7447  wemapso2lem  7452  unxpwdom2  7489  sucprcreg  7500  inf3lem2  7517  cantnfp1lem3  7569  cantnfp1  7570  setind  7606  r1tr  7635  r1ordg  7637  rankelb  7683  rankxplim3  7738  cardlim  7792  infxpenlem  7828  infxpenc2  7836  dfac5lem4  7940  dfac12k  7960  kmlem13  7975  sornom  8090  fin23lem25  8137  fin23lem21  8152  zorn2lem4  8312  iundom2g  8348  fpwwe2lem12  8449  fpwwe2lem13  8450  pwfseqlem4a  8469  eltsk2g  8559  inttsk  8582  tskord  8588  r1tskina  8590  grudomon  8625  arch  10150  zaddcl  10249  uzm1  10448  xrsupsslem  10817  xrinfmsslem  10818  fsequb  11241  fseqsupubi  11244  seqf1o  11291  sq01  11428  rexanre  12077  rexuzre  12083  cau3lem  12085  o1co  12307  rlimcn2  12311  o1of2  12333  lo1add  12347  lo1mul  12348  climcau  12391  climbdd  12392  caucvgb  12400  summo  12438  isumltss  12555  mertenslem2  12589  bitsfzolem  12873  bitsfzo  12874  bezoutlem4  12968  prmind2  13017  isprm5  13039  pcqmul  13154  pcadd  13185  prmreclem2  13212  prmreclem5  13215  mul4sq  13249  vdwmc2  13274  ramcl  13324  prmlem1a  13356  divsfval  13699  iscatd2  13833  catpropd  13862  wunfunc  14023  gaorber  15012  lsmsubm  15214  pj1eu  15255  efgredlem  15306  divsabl  15407  cygabl  15427  cygctb  15428  lt6abl  15431  gsumval3eu  15440  dprdsubg  15509  ablfac1c  15556  pgpfac1  15565  dvdsrtr  15684  unitgrp  15699  drngmul0or  15783  lvecvs0or  16107  lspdisjb  16125  lspsolvlem  16141  lspprat  16152  lbsextlem2  16158  abvn0b  16289  domnchr  16736  znfld  16764  cygznlem3  16773  obselocv  16878  0ntr  17058  opnneiid  17113  restntr  17168  hausnei2  17339  nrmsep3  17341  cmpsub  17385  uncmp  17388  dfcon2  17403  cnconn  17406  1stcfb  17429  txuni2  17518  txbas  17520  ptbasin  17530  txcls  17557  txbasval  17559  txlly  17589  txnlly  17590  pthaus  17591  txlm  17601  tx1stc  17603  xkohaus  17606  isufil2  17861  ufileu  17872  cnpflfi  17952  txflf  17959  fclscf  17978  flimfnfcls  17981  alexsubb  17998  alexsubALTlem2  18000  alexsubALTlem4  18002  ptcmplem2  18005  ptcmplem3  18006  cnextcn  18019  divstgplem  18071  prdsmet  18308  blin2  18349  prdsbl  18411  nmolb  18622  tgqioo  18702  reconnlem2  18729  reconn  18730  lebnumlem3  18859  iscau4  19103  cmetcaulem  19112  iscmet3lem2  19116  bcthlem5  19150  minveclem3b  19196  pmltpc  19214  evthicc2  19224  ovolunlem2  19261  ovolicc2lem5  19284  mblsplit  19295  iundisj2  19310  volsup  19317  ioombl1lem4  19322  dyaddisj  19355  dyadmbllem  19358  i1faddlem  19452  itg10a  19469  itg1ge0a  19470  mbfi1flimlem  19481  mbfmullem  19484  itg2add  19518  rolle  19741  dvcvx  19771  itgsubst  19800  tdeglem4  19850  ply1domn  19913  fta1b  19959  plyadd  20003  plymul  20004  coeeu  20011  vieta1  20096  aalioulem6  20121  ulmcaulem  20177  ulmcau  20178  ulmbdd  20181  ulmcn  20182  amgm  20696  mumullem2  20830  ppiublem1  20853  dchrfi  20906  dchrptlem2  20916  dchrptlem3  20917  dchrsum2  20919  lgsdchr  20999  lgsquad2lem2  21010  2sqlem5  21019  2sqb  21029  pntlemp  21171  ostthlem2  21189  ostth  21200  usgra2edg  21268  nvmul0or  21981  ubthlem3  22222  axhcompl-zf  22349  hvmul0or  22375  ocnel  22648  pjhthmo  22652  spanuni  22894  spansni  22907  hon0  23144  leopadd  23483  leoptr  23488  mdsymlem6  23759  sumdmdlem2  23770  cdjreui  23783  iundisj2f  23873  iundisj2fi  23991  voliune  24379  volfiniune  24380  ballotlemimin  24542  txscon  24707  cvmsdisj  24736  cvmliftlem15  24764  cvmlift2lem10  24778  cvmlift3lem7  24791  prodmolem2  25040  prodmo  25041  dfon2lem3  25165  dfon2lem5  25167  dfon2lem6  25168  dfon2lem7  25169  dfon2lem8  25170  soseq  25278  frr3g  25304  nodenselem4  25362  nodenselem5  25363  nobndup  25378  nobnddown  25379  axcontlem8  25624  axcontlem9  25625  ifscgr  25692  cgr3tr4  25700  btwnconn1lem13  25747  seglecgr12  25759  itg2addnc  25959  elicc3  26011  neibastop1  26079  tailfb  26097  fdc  26140  riscer  26295  intidl  26330  ispridlc  26371  prtlem14  26414  prtlem17  26416  diophin  26522  diophun  26523  psgneu  27098  pm10.57  27235  fnchoice  27368  bnj23  28421  bnj594  28621  bnj849  28634  ax10NEW7  28811  lpssat  29128  lssatle  29130  lshpkrlem6  29230  cvrnbtwn  29386  atlatmstc  29434  atlatle  29435  atlrelat1  29436  2at0mat0  29639  trlator0  30285  cdleme0moN  30339  cdlemn11pre  31325  dihord2pre  31340  dihmeetlem20N  31441  dochkrshp4  31504  lcfl6  31615
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator