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  1593  19.33b  1597  ax10  1886  necon4bd  2510  ceqex  2900  ssdisj  3506  pssdifn0  3517  disjss3  4024  somo  4350  frminex  4375  ordelord  4416  unizlim  4511  tfinds  4652  tfindsg  4653  tfindes  4655  tfinds2  4656  findsg  4685  sofld  5123  funopfv  5564  mpteqb  5616  suppssr  5661  funfvima  5755  fliftfun  5813  weniso  5854  frxp  6227  rdgsucmptnf  6444  frsucmptn  6453  tz7.49  6459  om00  6575  oewordi  6591  iiner  6733  eroveu  6755  th3qlem1  6766  undom  6952  sdomdif  7011  php3  7049  sucdom2  7059  unxpdomlem3  7071  fisseneq  7076  pssnn  7083  ordunifi  7109  isfinite2  7117  fiint  7135  ixpfi2  7156  finsschain  7164  ordtypelem10  7244  wofib  7262  wemapso2lem  7267  unxpwdom2  7304  sucprcreg  7315  inf3lem2  7332  cantnfp1lem3  7384  cantnfp1  7385  setind  7421  r1tr  7450  r1ordg  7452  rankelb  7498  rankxplim3  7553  cardlim  7607  infxpenlem  7643  infxpenc2  7651  dfac5lem4  7755  dfac12k  7775  kmlem13  7790  sornom  7905  fin23lem25  7952  fin23lem21  7967  zorn2lem4  8128  iundom2g  8164  fpwwe2lem12  8265  fpwwe2lem13  8266  pwfseqlem4a  8285  eltsk2g  8375  inttsk  8398  tskord  8404  r1tskina  8406  grudomon  8441  arch  9964  zaddcl  10061  uzm1  10260  xrsupsslem  10627  xrinfmsslem  10628  fsequb  11039  fseqsupubi  11042  seqf1o  11089  sq01  11225  rexanre  11832  rexuzre  11838  cau3lem  11840  o1co  12062  rlimcn2  12066  o1of2  12088  lo1add  12102  lo1mul  12103  climcau  12146  caucvgb  12154  summo  12192  isumltss  12309  mertenslem2  12343  bitsfzolem  12627  bitsfzo  12628  bezoutlem4  12722  prmind2  12771  isprm5  12793  pcqmul  12908  pcadd  12939  prmreclem2  12966  prmreclem5  12969  mul4sq  13003  vdwmc2  13028  ramcl  13078  prmlem1a  13110  divsfval  13451  iscatd2  13585  catpropd  13614  wunfunc  13775  gaorber  14764  lsmsubm  14966  pj1eu  15007  efgredlem  15058  divsabl  15159  cygabl  15179  cygctb  15180  lt6abl  15183  gsumval3eu  15192  dprdsubg  15261  ablfac1c  15308  pgpfac1  15317  dvdsrtr  15436  unitgrp  15451  drngmul0or  15535  lvecvs0or  15863  lspdisjb  15881  lspsolvlem  15897  lspprat  15908  lbsextlem2  15914  abvn0b  16045  domnchr  16488  znfld  16516  cygznlem3  16525  obselocv  16630  0ntr  16810  opnneiid  16865  restntr  16914  hausnei2  17083  nrmsep3  17085  cmpsub  17129  uncmp  17132  dfcon2  17147  cnconn  17150  1stcfb  17173  txuni2  17262  txbas  17264  ptbasin  17274  txcls  17301  txbasval  17303  txlly  17332  txnlly  17333  pthaus  17334  txlm  17344  tx1stc  17346  xkohaus  17349  isufil2  17605  ufileu  17616  cnpflfi  17696  txflf  17703  fclscf  17722  flimfnfcls  17725  alexsubb  17742  alexsubALTlem2  17744  alexsubALTlem4  17746  ptcmplem2  17749  ptcmplem3  17750  divstgplem  17805  prdsmet  17936  blin2  17977  prdsbl  18039  nmolb  18228  tgqioo  18308  reconnlem2  18334  reconn  18335  lebnumlem3  18463  iscau4  18707  cmetcaulem  18716  iscmet3lem2  18720  bcthlem5  18752  minveclem3b  18794  pmltpc  18812  evthicc2  18822  ovolunlem2  18859  ovolicc2lem5  18882  mblsplit  18893  iundisj2  18908  volsup  18915  ioombl1lem4  18920  dyaddisj  18953  dyadmbllem  18956  i1faddlem  19050  itg10a  19067  itg1ge0a  19068  mbfi1flimlem  19079  mbfmullem  19082  itg2add  19116  rolle  19339  dvcvx  19369  itgsubst  19398  tdeglem4  19448  ply1domn  19511  fta1b  19557  plyadd  19601  plymul  19602  coeeu  19609  vieta1  19694  aalioulem6  19719  ulmcaulem  19773  ulmcau  19774  ulmbdd  19777  ulmcn  19778  amgm  20287  mumullem2  20420  ppiublem1  20443  dchrfi  20496  dchrptlem2  20506  dchrptlem3  20507  dchrsum2  20509  lgsdchr  20589  lgsquad2lem2  20600  2sqlem5  20609  2sqb  20619  pntlemp  20761  ostthlem2  20779  ostth  20790  nvmul0or  21212  ubthlem3  21453  axhcompl-zf  21580  hvmul0or  21606  ocnel  21879  pjhthmo  21883  spanuni  22125  spansni  22138  hon0  22375  leopadd  22714  leoptr  22719  mdsymlem6  22990  sumdmdlem2  23001  cdjreui  23014  ballotlemimin  23066  iundisj2fi  23366  iundisj2f  23368  txscon  23774  cvmsdisj  23803  cvmliftlem15  23831  cvmlift2lem10  23845  cvmlift3lem7  23858  dfon2lem3  24143  dfon2lem5  24145  dfon2lem6  24146  dfon2lem7  24147  dfon2lem8  24148  soseq  24256  frr3g  24282  nodenselem4  24340  nodenselem5  24341  nobndup  24356  nobnddown  24357  funpartfun  24483  axcontlem8  24601  axcontlem9  24602  ifscgr  24669  cgr3tr4  24677  btwnconn1lem13  24724  seglecgr12  24736  itg2addnc  24935  isunscov  25085  sssu  25152  svli2  25495  qusp  25553  iintlem1  25621  elicc3  26239  neibastop1  26319  tailfb  26337  fdc  26466  riscer  26630  intidl  26665  ispridlc  26706  prtlem14  26753  prtlem17  26755  diophin  26863  diophun  26864  psgneu  27440  pm10.57  27577  fnchoice  27711  bnj23  28817  bnj594  29017  bnj849  29030  ax12-2  29176  a12studyALT  29206  lpssat  29276  lssatle  29278  lshpkrlem6  29378  cvrnbtwn  29534  atlatmstc  29582  atlatle  29583  atlrelat1  29584  2at0mat0  29787  trlator0  30433  cdleme0moN  30487  cdlemn11pre  31473  dihord2pre  31488  dihmeetlem20N  31589  dochkrshp4  31652  lcfl6  31763
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