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

Theorem syl5bir 218
Description: A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 21-Jun-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 206 . 2  |-  ( ph  ->  ps )
3 syl5bir.2 . 2  |-  ( ch 
->  ( ps  ->  th )
)
42, 3syl5 32 1  |-  ( ch 
->  ( ph  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185
This theorem is referenced by:  3imtr3g  269  oplem1  964  nic-ax  1506  19.30  1693  19.33b  1697  hbnt  1895  necon1bd  2675  necon4bdOLD  2680  ssdisj  3879  pssdifn0  3891  disjss3  4455  somo  4843  frminex  4868  ordelord  4909  unizlim  5003  sofld  5461  f0rn0  5776  funopfv  5912  mpteqb  5971  suppssrOLD  6022  fvrnressn  6087  funfvima  6148  fliftfun  6211  weniso  6251  tfinds  6693  tfindsg  6694  tfindes  6696  tfinds2  6697  findsg  6726  frxp  6909  suppssr  6949  rdgsucmptnf  7113  frsucmptn  7122  tz7.49  7128  om00  7242  oewordi  7258  iiner  7401  eroveu  7424  undom  7624  sdomdif  7684  php3  7722  sucdom2  7733  unxpdomlem3  7745  fisseneq  7750  pssnn  7757  ordunifi  7788  isfinite2  7796  fiint  7815  infssuni  7829  ixpfi2  7836  finsschain  7845  ordtypelem10  7970  wofib  7988  wemapsolem  7993  unxpwdom2  8032  inf3lem2  8063  cantnfp1lem3  8116  cantnfp1  8117  cantnfp1lem3OLD  8142  cantnfp1OLD  8143  setind  8182  r1tr  8211  r1ordg  8213  rankelb  8259  rankxplim3  8316  cardlim  8370  infxpenlem  8408  infxpenc2  8416  infxpenc2OLD  8420  dfac5lem4  8524  dfac12k  8544  kmlem13  8559  sornom  8674  fin23lem25  8721  fin23lem21  8736  zorn2lem4  8896  iundom2g  8932  fpwwe2lem12  9036  fpwwe2lem13  9037  pwfseqlem4a  9056  eltsk2g  9146  inttsk  9169  tskord  9175  r1tskina  9177  grudomon  9212  arch  10813  zaddcl  10925  uzm1  11136  xrsupsslem  11523  xrinfmsslem  11524  fsequb  12088  fseqsupubi  12091  ssnn0fi  12097  seqf1o  12151  sq01  12291  swrdccatin1  12720  repsdf2  12762  cshw1  12802  rexanre  13191  rexuzre  13197  cau3lem  13199  o1co  13421  rlimcn2  13425  o1of2  13447  lo1add  13461  lo1mul  13462  climcau  13505  climbdd  13506  caucvgb  13514  summo  13551  isumltss  13672  mertenslem2  13706  prodmolem2  13754  prodmo  13755  bitsfzolem  14096  bitsfzo  14097  bezoutlem4  14191  prmind2  14240  isprm5  14265  pcqmul  14389  pcadd  14420  prmreclem2  14447  prmreclem5  14450  mul4sq  14484  vdwmc2  14509  ramcl  14559  prmlem1a  14604  divsfval  14964  iscatd2  15098  catpropd  15125  wunfunc  15315  gaorber  16473  psgneu  16658  lsmsubm  16800  pj1eu  16841  efgredlem  16892  qusabl  16998  cygabl  17020  cygctb  17021  lt6abl  17024  gsumval3eu  17034  dprdsubg  17198  ablfac1c  17249  pgpfac1  17258  dvdsrtr  17428  unitgrp  17443  drngmul0or  17544  lvecvs0or  17881  lspdisjb  17899  lspsolvlem  17915  lspprat  17926  lbsextlem2  17932  abvn0b  18078  domnchr  18696  znfld  18726  cygznlem3  18735  obselocv  18886  cpmatacl  19344  chfacfisf  19482  chfacfisfcpmat  19483  0ntr  19699  opnneiid  19754  restntr  19810  hausnei2  19981  nrmsep3  19983  cmpsub  20027  uncmp  20030  dfcon2  20046  cnconn  20049  1stcfb  20072  txuni2  20192  txbas  20194  ptbasin  20204  txcls  20231  txbasval  20233  txlly  20263  txnlly  20264  pthaus  20265  txlm  20275  tx1stc  20277  xkohaus  20280  isufil2  20535  ufileu  20546  cnpflfi  20626  txflf  20633  fclscf  20652  flimfnfcls  20655  alexsubb  20672  alexsubALTlem2  20674  alexsubALTlem4  20676  ptcmplem2  20679  ptcmplem3  20680  cnextcn  20693  qustgplem  20745  prdsmet  20999  blin2  21058  prdsbl  21120  nmolb  21350  tgqioo  21431  reconnlem2  21458  reconn  21459  lebnumlem3  21589  iscau4  21844  cmetcaulem  21853  iscmet3lem2  21857  bcthlem5  21893  minveclem3b  21969  pmltpc  21988  evthicc2  21998  ovolunlem2  22035  ovolicc2lem5  22058  mblsplit  22069  iundisj2  22085  volsup  22092  ioombl1lem4  22097  dyaddisj  22131  dyadmbllem  22134  i1faddlem  22226  itg10a  22243  itg1ge0a  22244  mbfi1flimlem  22255  mbfmullem  22258  itg2add  22292  rolle  22517  dvcvx  22547  itgsubst  22576  tdeglem4  22584  ply1domn  22650  fta1b  22696  plyadd  22740  plymul  22741  coeeu  22748  vieta1  22834  aalioulem6  22859  ulmcaulem  22915  ulmcau  22916  ulmbdd  22919  ulmcn  22920  amgm  23446  mumullem2  23580  ppiublem1  23603  dchrfi  23656  dchrptlem2  23666  dchrptlem3  23667  dchrsum2  23669  lgsdchr  23749  lgsquad2lem2  23760  2sqlem5  23769  2sqb  23779  pntlemp  23921  ostthlem2  23939  ostth  23950  tgbtwnconn1  24088  colline  24156  lmimid  24285  axcontlem8  24401  axcontlem9  24402  eengtrkg  24415  usgra2edg  24509  usg2wlkeq  24835  clwlkisclwwlklem2a4  24911  clwwisshclwwn  24935  frgraregord013  25245  nvmul0or  25674  ubthlem3  25915  axhcompl-zf  26042  hvmul0or  26069  ocnel  26343  pjhthmo  26347  spanuni  26589  spansni  26602  hon0  26839  leopadd  27178  leoptr  27183  mdsymlem6  27454  sumdmdlem2  27465  cdjreui  27478  spc2d  27500  iundisj2f  27589  disjunsn  27593  iundisj2fi  27762  ballotlemimin  28641  txscon  28883  cvmsdisj  28912  cvmliftlem15  28940  cvmlift2lem10  28954  cvmlift3lem7  28967  mclsppslem  29140  dfon2lem3  29434  dfon2lem5  29436  dfon2lem6  29437  dfon2lem7  29438  dfon2lem8  29439  soseq  29551  frr3g  29603  nodenselem4  29661  nodenselem5  29662  nobndup  29677  nobnddown  29678  ifscgr  29899  cgr3tr4  29907  btwnconn1lem13  29954  seglecgr12  29966  wl-equsal1i  30201  ismblfin  30260  itg2addnclem3  30273  ftc1anclem6  30300  elicc3  30340  neibastop1  30382  tailfb  30400  fdc  30443  riscer  30596  intidl  30631  ispridlc  30672  prtlem14  30820  prtlem17  30822  diophin  30911  diophun  30912  pm10.57  31480  fnchoice  31607  ellimcabssub0  31826  fourierdlem81  32173  fourierdlem93  32185  cshword2  32555  ralnralall  32558  2ffzoeq  32605  nzerooringczr  33024  ply1mulgsumlem1  33130  snlindsntor  33216  islininds2  33229  bnj23  33914  bnj594  34113  bnj849  34126  bj-sngltag  34684  bj-elid  34742  lpssat  34881  lssatle  34883  lshpkrlem6  34983  cvrnbtwn  35139  atlatmstc  35187  atlatle  35188  atlrelat1  35189  2at0mat0  35392  trlator0  36039  cdleme0moN  36093  cdlemn11pre  37080  dihord2pre  37095  dihmeetlem20N  37196  dochkrshp4  37259  lcfl6  37370
  Copyright terms: Public domain W3C validator