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

Theorem syl5bir 222
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 210 . 2  |-  ( ph  ->  ps )
3 syl5bir.2 . 2  |-  ( ch 
->  ( ps  ->  th )
)
42, 3syl5 33 1  |-  ( ch 
->  ( ph  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188
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 189
This theorem is referenced by:  3imtr3g  273  oplem1  975  nic-ax  1556  19.30  1744  19.33b  1748  hbnt  1976  necon1bd  2642  ssdisj  3814  pssdifn0  3827  disjss3  4401  somo  4789  frminex  4814  sofld  5284  ordelord  5445  unizlim  5539  f0rn0  5768  funopfv  5904  mpteqb  5964  fvrnressn  6079  funfvima  6140  fliftfun  6205  weniso  6245  tfinds  6686  tfindsg  6687  tfindes  6689  tfinds2  6690  findsg  6720  frxp  6906  suppssr  6946  rdgsucmptnf  7147  frsucmptn  7156  tz7.49  7162  om00  7276  oewordi  7292  iiner  7435  eroveu  7458  undom  7660  sdomdif  7720  php3  7758  sucdom2  7768  unxpdomlem3  7778  fisseneq  7783  pssnn  7790  ordunifi  7821  isfinite2  7829  fiint  7848  infssuni  7865  ixpfi2  7872  finsschain  7881  ordtypelem10  8042  wofib  8060  wemapsolem  8065  unxpwdom2  8103  inf3lem2  8134  cantnfp1lem3  8185  cantnfp1  8186  setind  8218  r1tr  8247  r1ordg  8249  rankelb  8295  rankxplim3  8352  cardlim  8406  infxpenlem  8444  infxpenc2  8453  dfac5lem4  8557  dfac12k  8577  kmlem13  8592  sornom  8707  fin23lem25  8754  fin23lem21  8769  zorn2lem4  8929  iundom2g  8965  fpwwe2lem12  9066  fpwwe2lem13  9067  pwfseqlem4a  9086  eltsk2g  9176  inttsk  9199  tskord  9205  r1tskina  9207  grudomon  9242  arch  10866  zaddcl  10977  uzm1  11189  xrsupsslem  11592  xrinfmsslem  11593  fsequb  12188  fseqsupubi  12191  ssnn0fi  12197  seqf1o  12254  sq01  12394  swrdccatin1  12839  repsdf2  12881  cshw1  12921  rexanre  13409  rexuzre  13415  cau3lem  13417  o1co  13650  rlimcn2  13654  o1of2  13676  lo1add  13690  lo1mul  13691  climcau  13734  climbdd  13735  caucvgb  13746  summo  13783  isumltss  13906  mertenslem2  13941  prodmolem2  13989  prodmo  13990  bitsfzolem  14407  bitsfzolemOLD  14408  bitsfzo  14409  bezoutlem4OLD  14506  bezoutlem4  14509  lcmfeq0b  14603  lcmfunsnlem2  14613  prmind2  14635  isprm5  14651  pcqmul  14803  pcadd  14834  prmreclem2  14861  prmreclem5  14864  mul4sq  14898  vdwmc2  14929  ramcl  14987  prmgaplem7  15027  prmlem1a  15078  divsfval  15453  iscatd2  15587  catpropd  15614  wunfunc  15804  gaorber  16962  psgneu  17147  lsmsubm  17305  pj1eu  17346  efgredlem  17397  qusabl  17503  cygabl  17525  cygctb  17526  lt6abl  17529  gsumval3eu  17538  dprdsubg  17657  ablfac1c  17704  pgpfac1  17713  dvdsrtr  17880  unitgrp  17895  drngmul0or  17996  lvecvs0or  18331  lspdisjb  18349  lspsolvlem  18365  lspprat  18376  lbsextlem2  18382  abvn0b  18526  domnchr  19103  znfld  19131  cygznlem3  19140  obselocv  19291  cpmatacl  19740  chfacfisf  19878  chfacfisfcpmat  19879  0ntr  20087  opnneiid  20142  restntr  20198  hausnei2  20369  nrmsep3  20371  cmpsub  20415  uncmp  20418  dfcon2  20434  cnconn  20437  1stcfb  20460  txuni2  20580  txbas  20582  ptbasin  20592  txcls  20619  txbasval  20621  txlly  20651  txnlly  20652  pthaus  20653  txlm  20663  tx1stc  20665  xkohaus  20668  isufil2  20923  ufileu  20934  cnpflfi  21014  txflf  21021  fclscf  21040  flimfnfcls  21043  alexsubb  21061  alexsubALTlem2  21063  alexsubALTlem4  21065  ptcmplem2  21068  ptcmplem3  21069  cnextcn  21082  qustgplem  21135  prdsmet  21385  blin2  21444  prdsbl  21506  nmolb  21722  nmolbOLD  21741  tgqioo  21818  reconnlem2  21845  reconn  21846  lebnumlem3  21991  lebnumlem3OLD  21994  iscau4  22249  cmetcaulem  22258  iscmet3lem2  22262  bcthlem5  22296  minveclem3b  22370  minveclem3bOLD  22382  pmltpc  22401  evthicc2  22411  ovolunlem2  22451  ovolicc2lem5  22475  mblsplit  22486  iundisj2  22502  volsup  22509  ioombl1lem4  22514  dyaddisj  22554  dyadmbllem  22557  i1faddlem  22651  itg10a  22668  itg1ge0a  22669  mbfi1flimlem  22680  mbfmullem  22683  itg2add  22717  rolle  22942  dvcvx  22972  itgsubst  23001  tdeglem4  23009  ply1domn  23072  fta1b  23120  plyadd  23171  plymul  23172  coeeu  23179  vieta1  23265  aalioulem6  23293  ulmcaulem  23349  ulmcau  23350  ulmbdd  23353  ulmcn  23354  amgm  23916  mumullem2  24107  ppiublem1  24130  dchrfi  24183  dchrptlem2  24193  dchrptlem3  24194  dchrsum2  24196  lgsdchr  24276  lgsquad2lem2  24287  2sqlem5  24296  2sqb  24306  pntlemp  24448  ostthlem2  24466  ostth  24477  iscgrglt  24559  tgbtwnconn1  24620  colline  24694  lmimid  24836  axcontlem8  25001  axcontlem9  25002  eengtrkg  25015  usgra2edg  25109  usg2wlkeq  25436  clwlkisclwwlklem2a4  25512  clwwisshclwwn  25536  frgraregord013  25846  nvmul0or  26273  ubthlem3  26514  axhcompl-zf  26651  hvmul0or  26678  ocnel  26951  pjhthmo  26955  spanuni  27197  spansni  27210  hon0  27446  leopadd  27785  leoptr  27790  mdsymlem6  28061  sumdmdlem2  28072  cdjreui  28085  spc2d  28107  iundisj2f  28200  disjunsn  28204  iundisj2fi  28373  ballotlemimin  29338  ballotlemiminOLD  29376  bnj23  29524  bnj594  29723  bnj849  29736  txscon  29964  cvmsdisj  29993  cvmliftlem15  30021  cvmlift2lem10  30035  cvmlift3lem7  30048  mclsppslem  30221  dfon2lem3  30431  dfon2lem5  30433  dfon2lem6  30434  dfon2lem7  30435  dfon2lem8  30436  soseq  30492  frr3g  30513  nodenselem4  30573  nodenselem5  30574  nobndup  30589  nobnddown  30590  ifscgr  30811  cgr3tr4  30819  btwnconn1lem13  30866  seglecgr12  30878  elicc3  30973  neibastop1  31015  tailfb  31033  bj-sngltag  31577  bj-elid  31640  mptsnunlem  31740  finxpreclem6  31788  wl-equsal1i  31876  poimirlem26  31966  poimirlem27  31967  ismblfin  31981  itg2addnclem3  31995  ftc1anclem6  32022  fdc  32074  riscer  32227  intidl  32262  ispridlc  32303  prtlem14  32446  prtlem17  32448  lpssat  32579  lssatle  32581  lshpkrlem6  32681  cvrnbtwn  32837  atlatmstc  32885  atlatle  32886  atlrelat1  32887  2at0mat0  33090  trlator0  33737  cdleme0moN  33791  cdlemn11pre  34778  dihord2pre  34793  dihmeetlem20N  34894  dochkrshp4  34957  lcfl6  35068  diophin  35615  diophun  35616  pm10.57  36720  fnchoice  37350  ellimcabssub0  37697  fourierdlem81  38051  fourierdlem93  38063  fzopredsuc  38720  iccpartlt  38738  bgoldbst  38879  nnsum4primesevenALTV  38896  cshword2  38978  ralnralall  38985  fpropnf1  39036  2ffzoeq  39064  structgrssvtxlem  39125  usgr2edg  39291  nzerooringczr  40127  ply1mulgsumlem1  40231  snlindsntor  40317  islininds2  40330  m1modmmod  40377
  Copyright terms: Public domain W3C validator