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  1594  19.33b  1598  ax10  1897  necon4bd  2521  ceqex  2911  ssdisj  3517  pssdifn0  3528  disjss3  4038  somo  4364  frminex  4389  ordelord  4430  unizlim  4525  tfinds  4666  tfindsg  4667  tfindes  4669  tfinds2  4670  findsg  4699  sofld  5137  funopfv  5578  mpteqb  5630  suppssr  5675  funfvima  5769  fliftfun  5827  weniso  5868  frxp  6241  rdgsucmptnf  6458  frsucmptn  6467  tz7.49  6473  om00  6589  oewordi  6605  iiner  6747  eroveu  6769  th3qlem1  6780  undom  6966  sdomdif  7025  php3  7063  sucdom2  7073  unxpdomlem3  7085  fisseneq  7090  pssnn  7097  ordunifi  7123  isfinite2  7131  fiint  7149  ixpfi2  7170  finsschain  7178  ordtypelem10  7258  wofib  7276  wemapso2lem  7281  unxpwdom2  7318  sucprcreg  7329  inf3lem2  7346  cantnfp1lem3  7398  cantnfp1  7399  setind  7435  r1tr  7464  r1ordg  7466  rankelb  7512  rankxplim3  7567  cardlim  7621  infxpenlem  7657  infxpenc2  7665  dfac5lem4  7769  dfac12k  7789  kmlem13  7804  sornom  7919  fin23lem25  7966  fin23lem21  7981  zorn2lem4  8142  iundom2g  8178  fpwwe2lem12  8279  fpwwe2lem13  8280  pwfseqlem4a  8299  eltsk2g  8389  inttsk  8412  tskord  8418  r1tskina  8420  grudomon  8455  arch  9978  zaddcl  10075  uzm1  10274  xrsupsslem  10641  xrinfmsslem  10642  fsequb  11053  fseqsupubi  11056  seqf1o  11103  sq01  11239  rexanre  11846  rexuzre  11852  cau3lem  11854  o1co  12076  rlimcn2  12080  o1of2  12102  lo1add  12116  lo1mul  12117  climcau  12160  caucvgb  12168  summo  12206  isumltss  12323  mertenslem2  12357  bitsfzolem  12641  bitsfzo  12642  bezoutlem4  12736  prmind2  12785  isprm5  12807  pcqmul  12922  pcadd  12953  prmreclem2  12980  prmreclem5  12983  mul4sq  13017  vdwmc2  13042  ramcl  13092  prmlem1a  13124  divsfval  13465  iscatd2  13599  catpropd  13628  wunfunc  13789  gaorber  14778  lsmsubm  14980  pj1eu  15021  efgredlem  15072  divsabl  15173  cygabl  15193  cygctb  15194  lt6abl  15197  gsumval3eu  15206  dprdsubg  15275  ablfac1c  15322  pgpfac1  15331  dvdsrtr  15450  unitgrp  15465  drngmul0or  15549  lvecvs0or  15877  lspdisjb  15895  lspsolvlem  15911  lspprat  15922  lbsextlem2  15928  abvn0b  16059  domnchr  16502  znfld  16530  cygznlem3  16539  obselocv  16644  0ntr  16824  opnneiid  16879  restntr  16928  hausnei2  17097  nrmsep3  17099  cmpsub  17143  uncmp  17146  dfcon2  17161  cnconn  17164  1stcfb  17187  txuni2  17276  txbas  17278  ptbasin  17288  txcls  17315  txbasval  17317  txlly  17346  txnlly  17347  pthaus  17348  txlm  17358  tx1stc  17360  xkohaus  17363  isufil2  17619  ufileu  17630  cnpflfi  17710  txflf  17717  fclscf  17736  flimfnfcls  17739  alexsubb  17756  alexsubALTlem2  17758  alexsubALTlem4  17760  ptcmplem2  17763  ptcmplem3  17764  divstgplem  17819  prdsmet  17950  blin2  17991  prdsbl  18053  nmolb  18242  tgqioo  18322  reconnlem2  18348  reconn  18349  lebnumlem3  18477  iscau4  18721  cmetcaulem  18730  iscmet3lem2  18734  bcthlem5  18766  minveclem3b  18808  pmltpc  18826  evthicc2  18836  ovolunlem2  18873  ovolicc2lem5  18896  mblsplit  18907  iundisj2  18922  volsup  18929  ioombl1lem4  18934  dyaddisj  18967  dyadmbllem  18970  i1faddlem  19064  itg10a  19081  itg1ge0a  19082  mbfi1flimlem  19093  mbfmullem  19096  itg2add  19130  rolle  19353  dvcvx  19383  itgsubst  19412  tdeglem4  19462  ply1domn  19525  fta1b  19571  plyadd  19615  plymul  19616  coeeu  19623  vieta1  19708  aalioulem6  19733  ulmcaulem  19787  ulmcau  19788  ulmbdd  19791  ulmcn  19792  amgm  20301  mumullem2  20434  ppiublem1  20457  dchrfi  20510  dchrptlem2  20520  dchrptlem3  20521  dchrsum2  20523  lgsdchr  20603  lgsquad2lem2  20614  2sqlem5  20623  2sqb  20633  pntlemp  20775  ostthlem2  20793  ostth  20804  nvmul0or  21226  ubthlem3  21467  axhcompl-zf  21594  hvmul0or  21620  ocnel  21893  pjhthmo  21897  spanuni  22139  spansni  22152  hon0  22389  leopadd  22728  leoptr  22733  mdsymlem6  23004  sumdmdlem2  23015  cdjreui  23028  ballotlemimin  23080  iundisj2fi  23379  iundisj2f  23381  txscon  23787  cvmsdisj  23816  cvmliftlem15  23844  cvmlift2lem10  23858  cvmlift3lem7  23871  prodmolem2  24158  prodmo  24159  dfon2lem3  24212  dfon2lem5  24214  dfon2lem6  24215  dfon2lem7  24216  dfon2lem8  24217  soseq  24325  frr3g  24351  nodenselem4  24409  nodenselem5  24410  nobndup  24425  nobnddown  24426  axcontlem8  24671  axcontlem9  24672  ifscgr  24739  cgr3tr4  24747  btwnconn1lem13  24794  seglecgr12  24806  itg2addnc  25005  isunscov  25177  sssu  25244  svli2  25587  qusp  25645  iintlem1  25713  elicc3  26331  neibastop1  26411  tailfb  26429  fdc  26558  riscer  26722  intidl  26757  ispridlc  26798  prtlem14  26845  prtlem17  26847  diophin  26955  diophun  26956  psgneu  27532  pm10.57  27669  fnchoice  27803  bnj23  29060  bnj594  29260  bnj849  29273  ax10NEW7  29450  ax12-2  29725  a12studyALT  29755  lpssat  29825  lssatle  29827  lshpkrlem6  29927  cvrnbtwn  30083  atlatmstc  30131  atlatle  30132  atlrelat1  30133  2at0mat0  30336  trlator0  30982  cdleme0moN  31036  cdlemn11pre  32022  dihord2pre  32037  dihmeetlem20N  32138  dochkrshp4  32201  lcfl6  32312
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