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  hbnt  1795  ax10OLD  1998  necon4bd  2629  ceqex  3026  ssdisj  3637  pssdifn0  3649  disjss3  4171  somo  4497  frminex  4522  ordelord  4563  unizlim  4657  tfinds  4798  tfindsg  4799  tfindes  4801  tfinds2  4802  findsg  4831  sofld  5277  funopfv  5725  mpteqb  5778  suppssr  5823  funfvima  5932  fliftfun  5993  weniso  6034  frxp  6415  rdgsucmptnf  6646  frsucmptn  6655  tz7.49  6661  om00  6777  oewordi  6793  iiner  6935  eroveu  6958  th3qlem1  6969  undom  7155  sdomdif  7214  php3  7252  sucdom2  7262  unxpdomlem3  7274  fisseneq  7279  pssnn  7286  ordunifi  7316  isfinite2  7324  fiint  7342  ixpfi2  7363  finsschain  7371  ordtypelem10  7452  wofib  7470  wemapso2lem  7475  unxpwdom2  7512  sucprcreg  7523  inf3lem2  7540  cantnfp1lem3  7592  cantnfp1  7593  setind  7629  r1tr  7658  r1ordg  7660  rankelb  7706  rankxplim3  7761  cardlim  7815  infxpenlem  7851  infxpenc2  7859  dfac5lem4  7963  dfac12k  7983  kmlem13  7998  sornom  8113  fin23lem25  8160  fin23lem21  8175  zorn2lem4  8335  iundom2g  8371  fpwwe2lem12  8472  fpwwe2lem13  8473  pwfseqlem4a  8492  eltsk2g  8582  inttsk  8605  tskord  8611  r1tskina  8613  grudomon  8648  arch  10174  zaddcl  10273  uzm1  10472  xrsupsslem  10841  xrinfmsslem  10842  fsequb  11269  fseqsupubi  11272  seqf1o  11319  sq01  11456  rexanre  12105  rexuzre  12111  cau3lem  12113  o1co  12335  rlimcn2  12339  o1of2  12361  lo1add  12375  lo1mul  12376  climcau  12419  climbdd  12420  caucvgb  12428  summo  12466  isumltss  12583  mertenslem2  12617  bitsfzolem  12901  bitsfzo  12902  bezoutlem4  12996  prmind2  13045  isprm5  13067  pcqmul  13182  pcadd  13213  prmreclem2  13240  prmreclem5  13243  mul4sq  13277  vdwmc2  13302  ramcl  13352  prmlem1a  13384  divsfval  13727  iscatd2  13861  catpropd  13890  wunfunc  14051  gaorber  15040  lsmsubm  15242  pj1eu  15283  efgredlem  15334  divsabl  15435  cygabl  15455  cygctb  15456  lt6abl  15459  gsumval3eu  15468  dprdsubg  15537  ablfac1c  15584  pgpfac1  15593  dvdsrtr  15712  unitgrp  15727  drngmul0or  15811  lvecvs0or  16135  lspdisjb  16153  lspsolvlem  16169  lspprat  16180  lbsextlem2  16186  abvn0b  16317  domnchr  16768  znfld  16796  cygznlem3  16805  obselocv  16910  0ntr  17090  opnneiid  17145  restntr  17200  hausnei2  17371  nrmsep3  17373  cmpsub  17417  uncmp  17420  dfcon2  17435  cnconn  17438  1stcfb  17461  txuni2  17550  txbas  17552  ptbasin  17562  txcls  17589  txbasval  17591  txlly  17621  txnlly  17622  pthaus  17623  txlm  17633  tx1stc  17635  xkohaus  17638  isufil2  17893  ufileu  17904  cnpflfi  17984  txflf  17991  fclscf  18010  flimfnfcls  18013  alexsubb  18030  alexsubALTlem2  18032  alexsubALTlem4  18034  ptcmplem2  18037  ptcmplem3  18038  cnextcn  18051  divstgplem  18103  prdsmet  18353  blin2  18412  prdsbl  18474  nmolb  18704  tgqioo  18784  reconnlem2  18811  reconn  18812  lebnumlem3  18941  iscau4  19185  cmetcaulem  19194  iscmet3lem2  19198  bcthlem5  19234  minveclem3b  19282  pmltpc  19300  evthicc2  19310  ovolunlem2  19347  ovolicc2lem5  19370  mblsplit  19381  iundisj2  19396  volsup  19403  ioombl1lem4  19408  dyaddisj  19441  dyadmbllem  19444  i1faddlem  19538  itg10a  19555  itg1ge0a  19556  mbfi1flimlem  19567  mbfmullem  19570  itg2add  19604  rolle  19827  dvcvx  19857  itgsubst  19886  tdeglem4  19936  ply1domn  19999  fta1b  20045  plyadd  20089  plymul  20090  coeeu  20097  vieta1  20182  aalioulem6  20207  ulmcaulem  20263  ulmcau  20264  ulmbdd  20267  ulmcn  20268  amgm  20782  mumullem2  20916  ppiublem1  20939  dchrfi  20992  dchrptlem2  21002  dchrptlem3  21003  dchrsum2  21005  lgsdchr  21085  lgsquad2lem2  21096  2sqlem5  21105  2sqb  21115  pntlemp  21257  ostthlem2  21275  ostth  21286  usgra2edg  21355  nvmul0or  22086  ubthlem3  22327  axhcompl-zf  22454  hvmul0or  22480  ocnel  22753  pjhthmo  22757  spanuni  22999  spansni  23012  hon0  23249  leopadd  23588  leoptr  23593  mdsymlem6  23864  sumdmdlem2  23875  cdjreui  23888  iundisj2f  23983  iundisj2fi  24106  voliune  24538  volfiniune  24539  ballotlemimin  24716  txscon  24881  cvmsdisj  24910  cvmliftlem15  24938  cvmlift2lem10  24952  cvmlift3lem7  24965  prodmolem2  25214  prodmo  25215  dfon2lem3  25355  dfon2lem5  25357  dfon2lem6  25358  dfon2lem7  25359  dfon2lem8  25360  soseq  25468  frr3g  25494  nodenselem4  25552  nodenselem5  25553  nobndup  25568  nobnddown  25569  axcontlem8  25814  axcontlem9  25815  ifscgr  25882  cgr3tr4  25890  btwnconn1lem13  25937  seglecgr12  25949  ismblfin  26146  itg2addnclem3  26157  elicc3  26210  neibastop1  26278  tailfb  26296  fdc  26339  riscer  26494  intidl  26529  ispridlc  26570  prtlem14  26613  prtlem17  26615  diophin  26721  diophun  26722  psgneu  27297  pm10.57  27434  fnchoice  27567  swrdccatin1  28016  swrdccatin12b  28027  bnj23  28789  bnj594  28989  bnj849  29002  ax10NEW7  29179  lpssat  29496  lssatle  29498  lshpkrlem6  29598  cvrnbtwn  29754  atlatmstc  29802  atlatle  29803  atlrelat1  29804  2at0mat0  30007  trlator0  30653  cdleme0moN  30707  cdlemn11pre  31693  dihord2pre  31708  dihmeetlem20N  31809  dochkrshp4  31872  lcfl6  31983
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