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

Theorem syl5bir 209
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 197 . 2  |-  ( ph  ->  ps )
3 syl5bir.2 . 2  |-  ( ch 
->  ( ps  ->  th )
)
42, 3syl5 28 1  |-  ( ch 
->  ( ph  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  3imtr3g  260  oplem1  930  nic-ax  1428  19.30  1591  19.33b  1595  ax10  1886  necon4bd  2509  ceqex  2899  ssdisj  3505  pssdifn0  3516  disjss3  4023  somo  4347  frminex  4372  ordelord  4413  unizlim  4508  tfinds  4649  tfindsg  4650  tfindes  4652  tfinds2  4653  findsg  4682  sofld  5120  funopfv  5524  mpteqb  5576  suppssr  5621  funfvima  5715  fliftfun  5773  weniso  5814  frxp  6187  rdgsucmptnf  6438  frsucmptn  6447  tz7.49  6453  om00  6569  oewordi  6585  iiner  6727  eroveu  6749  th3qlem1  6760  undom  6946  sdomdif  7005  php3  7043  sucdom2  7053  unxpdomlem3  7065  fisseneq  7070  pssnn  7077  ordunifi  7103  isfinite2  7111  fiint  7129  ixpfi2  7150  finsschain  7158  ordtypelem10  7238  wofib  7256  wemapso2lem  7261  unxpwdom2  7298  sucprcreg  7309  inf3lem2  7326  cantnfp1lem3  7378  cantnfp1  7379  setind  7415  r1tr  7444  r1ordg  7446  rankelb  7492  rankxplim3  7547  cardlim  7601  infxpenlem  7637  infxpenc2  7645  dfac5lem4  7749  dfac12k  7769  kmlem13  7784  sornom  7899  fin23lem25  7946  fin23lem21  7961  zorn2lem4  8122  iundom2g  8158  fpwwe2lem12  8259  fpwwe2lem13  8260  pwfseqlem4a  8279  eltsk2g  8369  inttsk  8392  tskord  8398  r1tskina  8400  grudomon  8435  arch  9958  zaddcl  10055  uzm1  10254  xrsupsslem  10621  xrinfmsslem  10622  fsequb  11033  fseqsupubi  11036  seqf1o  11083  sq01  11219  rexanre  11826  rexuzre  11832  cau3lem  11834  o1co  12056  rlimcn2  12060  o1of2  12082  lo1add  12096  lo1mul  12097  climcau  12140  caucvgb  12148  summo  12186  isumltss  12303  mertenslem2  12337  bitsfzolem  12621  bitsfzo  12622  bezoutlem4  12716  prmind2  12765  isprm5  12787  pcqmul  12902  pcadd  12933  prmreclem2  12960  prmreclem5  12963  mul4sq  12997  vdwmc2  13022  ramcl  13072  prmlem1a  13104  divsfval  13445  iscatd2  13579  catpropd  13608  wunfunc  13769  gaorber  14758  lsmsubm  14960  pj1eu  15001  efgredlem  15052  divsabl  15153  cygabl  15173  cygctb  15174  lt6abl  15177  gsumval3eu  15186  dprdsubg  15255  ablfac1c  15302  pgpfac1  15311  dvdsrtr  15430  unitgrp  15445  drngmul0or  15529  lvecvs0or  15857  lspdisjb  15875  lspsolvlem  15891  lspprat  15902  lbsextlem2  15908  abvn0b  16039  domnchr  16482  znfld  16510  cygznlem3  16519  obselocv  16624  0ntr  16804  opnneiid  16859  restntr  16908  hausnei2  17077  nrmsep3  17079  cmpsub  17123  uncmp  17126  dfcon2  17141  cnconn  17144  1stcfb  17167  txuni2  17256  txbas  17258  ptbasin  17268  txcls  17295  txbasval  17297  txlly  17326  txnlly  17327  pthaus  17328  txlm  17338  tx1stc  17340  xkohaus  17343  isufil2  17599  ufileu  17610  cnpflfi  17690  txflf  17697  fclscf  17716  flimfnfcls  17719  alexsubb  17736  alexsubALTlem2  17738  alexsubALTlem4  17740  ptcmplem2  17743  ptcmplem3  17744  divstgplem  17799  prdsmet  17930  blin2  17971  prdsbl  18033  nmolb  18222  tgqioo  18302  reconnlem2  18328  reconn  18329  lebnumlem3  18457  iscau4  18701  cmetcaulem  18710  iscmet3lem2  18714  bcthlem5  18746  minveclem3b  18788  pmltpc  18806  evthicc2  18816  ovolunlem2  18853  ovolicc2lem5  18876  mblsplit  18887  iundisj2  18902  volsup  18909  ioombl1lem4  18914  dyaddisj  18947  dyadmbllem  18950  i1faddlem  19044  itg10a  19061  itg1ge0a  19062  mbfi1flimlem  19073  mbfmullem  19076  itg2add  19110  rolle  19333  dvcvx  19363  itgsubst  19392  tdeglem4  19442  ply1domn  19505  fta1b  19551  plyadd  19595  plymul  19596  coeeu  19603  vieta1  19688  aalioulem6  19713  ulmcaulem  19767  ulmcau  19768  ulmbdd  19771  ulmcn  19772  amgm  20281  mumullem2  20414  ppiublem1  20437  dchrfi  20490  dchrptlem2  20500  dchrptlem3  20501  dchrsum2  20503  lgsdchr  20583  lgsquad2lem2  20594  2sqlem5  20603  2sqb  20613  pntlemp  20755  ostthlem2  20773  ostth  20784  nvmul0or  21204  ubthlem3  21445  axhcompl-zf  21574  hvmul0or  21600  ocnel  21873  pjhthmo  21877  spanuni  22119  spansni  22132  hon0  22369  leopadd  22708  leoptr  22713  mdsymlem6  22984  sumdmdlem2  22995  cdjreui  23008  ballotlemimin  23060  txscon  23179  cvmsdisj  23208  cvmliftlem15  23236  cvmlift2lem10  23250  cvmlift3lem7  23263  dfon2lem3  23545  dfon2lem5  23547  dfon2lem6  23548  dfon2lem7  23549  dfon2lem8  23550  soseq  23658  frr3g  23684  axdenselem4  23742  axdenselem5  23743  axfelem9  23758  axfelem10  23759  funpartfun  23891  axcontlem8  24009  axcontlem9  24010  ifscgr  24077  cgr3tr4  24085  btwnconn1lem13  24132  seglecgr12  24144  isunscov  24484  sssu  24552  svli2  24895  qusp  24953  iintlem1  25021  elicc3  25639  neibastop1  25719  tailfb  25737  fdc  25866  riscer  26030  intidl  26065  ispridlc  26106  prtlem14  26153  prtlem17  26155  diophin  26263  diophun  26264  psgneu  26840  pm10.57  26977  fnchoice  27111  bnj23  28023  bnj594  28223  bnj849  28236  ax12-2  28382  a12studyALT  28412  lpssat  28482  lssatle  28484  lshpkrlem6  28584  cvrnbtwn  28740  atlatmstc  28788  atlatle  28789  atlrelat1  28790  2at0mat0  28993  trlator0  29639  cdleme0moN  29693  cdlemn11pre  30679  dihord2pre  30694  dihmeetlem20N  30795  dochkrshp4  30858  lcfl6  30969
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 177
  Copyright terms: Public domain W3C validator