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

Theorem syl5ibr 229
Description: A mixed syllogism inference. (Contributed by NM, 3-Apr-1994.)
Hypotheses
Ref Expression
syl5ibr.1  |-  ( ph  ->  th )
syl5ibr.2  |-  ( ch 
->  ( ps  <->  th )
)
Assertion
Ref Expression
syl5ibr  |-  ( ch 
->  ( ph  ->  ps ) )

Proof of Theorem syl5ibr
StepHypRef Expression
1 syl5ibr.1 . 2  |-  ( ph  ->  th )
2 syl5ibr.2 . . 3  |-  ( ch 
->  ( ps  <->  th )
)
32bicomd 206 . 2  |-  ( ch 
->  ( th  <->  ps )
)
41, 3syl5ib 227 1  |-  ( ch 
->  ( ph  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189
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 190
This theorem is referenced by:  syl5ibrcom  230  biimprd  231  exdistrf  2182  pm2.61ne  2728  unineq  3684  elpreqprlem  4152  oteqex  4694  otel3xp  4875  elrnmpt1  5089  cnveqb  5298  cnveq0  5299  relcoi1OLD  5372  predpoirr  5415  predfrirr  5416  ordtri3  5466  limelon  5493  ndmfv  5903  ffvresb  6070  isomin  6246  isofrlem  6249  caovord3d  6498  eldifpw  6622  ssonuni  6632  onsucuni2  6680  ordzsl  6691  tfindsg  6706  findsg  6739  oteqimp  6831  frxp  6925  poxp  6927  fnwelem  6930  suppss  6964  wfrlem14  7067  tfrlem11  7124  oacl  7255  omcl  7256  oecl  7257  oa0r  7258  om0r  7259  om1r  7262  oe1m  7264  oaordi  7265  oawordri  7269  oaass  7280  oarec  7281  omwordri  7291  odi  7298  omass  7299  oewordri  7311  oeworde  7312  oeordsuc  7313  oelim2  7314  oeoa  7316  oeoelem  7317  oeoe  7318  nnm0r  7329  nnacl  7330  nnacom  7336  nnaordi  7337  nnaass  7341  nndi  7342  nnmass  7343  nnmsucr  7344  nnmcom  7345  omabs  7366  brecop  7474  eceqoveq  7486  elpm2r  7507  map0g  7529  undifixp  7576  fundmen  7661  mapxpen  7756  mapunen  7759  php  7774  unxpdomlem2  7795  pssnn  7808  f1vrnfibi  7877  elfir  7947  wemapso2lem  8085  wdompwdom  8111  inf3lem1  8151  inf3lem3  8153  cantnfval2  8192  cantnfp1lem3  8203  r1sdom  8263  r1tr  8265  carden2a  8418  fidomtri2  8446  prdom2  8455  infxpenlem  8462  acndom  8500  fodomacn  8505  wdomfil  8510  alephon  8518  alephordi  8523  alephle  8537  alephfplem3  8555  dfac2a  8578  kmlem9  8606  cflm  8698  cfslb  8714  cfslbn  8715  infpssrlem3  8753  infpssrlem4  8754  fin23lem21  8787  fin23lem30  8790  isf34lem7  8827  isf34lem6  8828  fin67  8843  isfin7-2  8844  fin1a2lem7  8854  fin1a2lem10  8857  iundom2g  8983  konigthlem  9011  alephreg  9025  gchdomtri  9072  wunr1om  9162  tskr1om  9210  inar1  9218  grur1a  9262  indpi  9350  genpprecl  9444  genpnmax  9450  addcmpblnr  9511  recexsrlem  9545  map2psrpr  9552  ax1rid  9603  axpre-mulgt0  9610  ltle  9740  nnmulcl  10654  nnsub  10670  nn0sub  10944  nneo  11042  uz11  11205  xrltle  11471  xltnegi  11532  xrsupsslem  11617  xrinfmsslem  11618  xrub  11622  supxrunb1  11630  supxrunb2  11631  om2uzuzi  12201  uzrdgxfr  12218  seqcl2  12269  seqfveq2  12273  seqshft2  12277  seqsplit  12284  seqcaopr3  12286  seqf1olem2a  12289  seqid2  12297  seqhomo  12298  ser1const  12307  m1expcl2  12332  expadd  12352  expmul  12355  faclbnd  12513  hashmap  12648  hashfacen  12658  hashf1lem1  12659  hashf1lem2  12660  hashf1  12661  seqcoll  12668  wrdsymb0  12752  swrdnd2  12843  wrd2ind  12888  swrdccatin12lem2  12899  swrdccatin1d  12909  repswccat  12942  repswcshw  12968  cshwcshid  12983  rtrclreclem3  13200  rtrclreclem4  13201  dfrtrcl2  13202  relexpindlem  13203  relexpind  13204  rtrclind  13205  recan  13476  rexanre  13486  rlimcn2  13731  caurcvg2  13821  fsumiun  13958  efexp  14232  rpnnen2  14355  dvdstr  14414  alzdvds  14432  bitsinv1  14495  smu01lem  14538  smupval  14541  smueqlem  14543  smumullem  14545  seq1st  14609  lcmfunsnlem2lem1  14690  lcmfunsnlem2lem2  14691  prmdiveq  14813  odzdvds  14819  odzdvdsOLD  14825  pythagtriplem2  14846  pcexp  14888  vdwlem13  15022  ramz  15062  prmolefac  15083  prmorlefacOLD  15097  elrestr  15405  xpsff1o  15552  subsubc  15836  clatl  16440  frmdgsum  16724  mulgneg2  16863  mulgnnass  16864  mhmmulg  16868  gsumwrev  17095  symgbas  17099  symgextf1lem  17139  symgfixelsi  17154  pmtrdifellem4  17198  sylow1lem1  17328  efgsfo  17467  efgred  17476  cyggexb  17611  gsumzres  17621  gsum2dlem2  17681  mulgass2  17907  lmodprop2d  18228  lspsnne2  18419  lspsneu  18424  assapropd  18628  mplcoe1  18766  mplcoe3  18767  mplcoe5  18769  ply1sclf1  18959  cnfldmulg  19077  cnfldexp  19078  zrhpsgnelbas  19239  mat1scmat  19641  restopn2  20270  cnpf2  20343  cmpfi  20500  txcn  20718  txlm  20740  xkoptsub  20746  xkopjcn  20748  ufildr  21024  cnflf  21095  fclsnei  21112  fclscmp  21123  ufilcmp  21125  cnfcf  21135  symgtgp  21194  isxms2  21541  met2ndc  21616  metustbl  21659  tngngp2  21738  clmmulg  22202  iscau4  22327  ovolunlem1a  22527  ovolicc2lem4OLD  22551  ovolicc2lem4  22552  volfiniun  22579  voliunlem1  22582  volsup  22588  dvnadd  22962  dvnres  22964  dvcobr  22979  ply1nzb  23150  plypf1  23245  dgrle  23276  coeaddlem  23282  dgrlt  23299  dvntaylp  23405  cxpmul2  23713  rlimcnp  23970  facgam  24070  wilthlem2  24073  isnsqf  24141  musum  24199  chtub  24219  chpval2  24225  dchrisumlem1  24406  qabvexp  24543  ostthlem2  24545  axsegconlem1  25026  ax5seglem4  25041  ax5seglem5  25042  axlowdimlem15  25065  axcontlem2  25074  axcontlem4  25076  ushgrauhgra  25109  usgra2edg  25188  cusgrafilem1  25286  sizeusglecusglem1  25291  sizeusglecusg  25293  trliswlk  25348  2trllemF  25358  constr3lem6  25456  1conngra  25482  wlkiswwlk2lem4  25501  wwlknredwwlkn0  25534  wwlkextwrd  25535  wwlkextproplem1  25548  wwlkextprop  25551  clwlkisclwwlklem2a  25592  clwwlkf1  25603  erclwwlksym  25621  eleclclwwlknlem2  25625  erclwwlknsym  25633  el2wlkonot  25676  el2spthonot  25677  hashnbgravdg  25720  eupatrl  25775  frgra3vlem1  25807  3vfriswmgralem  25811  frconngra  25828  frgrawopreglem3  25853  frg2wot1  25864  2spotiundisj  25869  usg2spot2nb  25872  usgreg2spot  25874  extwwlkfablem2  25885  numclwwlkovf2ex  25893  extwwlkfab  25897  isexid2  26134  ismndo1  26153  rngo2  26197  rngoueqz  26239  sspval  26443  nmosetre  26486  nmobndseqi  26501  nmobndseqiALT  26502  orthcom  26842  shsva  27054  shmodsi  27123  h1datomi  27315  nmopsetretALT  27597  nmfnsetre  27611  lnopcnbd  27770  pjclem4  27933  pj3si  27941  ssmd1  28045  atom1d  28087  chjatom  28091  atcvat4i  28131  cdj3lem2a  28170  cdj3lem3a  28173  disjunsn  28281  unitdivcld  28781  xrge0iifiso  28815  dya2iocuni  29178  bnj168  29610  bnj535  29773  bnj590  29793  bnj594  29795  bnj938  29820  bnj1118  29865  bnj1128  29871  deranglem  29961  subfacp1lem6  29980  subfacval2  29982  cvmlift2lem12  30109  mrsubvrs  30232  msrrcl  30253  mclsax  30279  dfon2lem6  30505  rdgprc  30512  trpredlem1  30539  frrlem5e  30593  nodenselem8  30648  ifscgr  30882  btwncolinear1  30907  hfelhf  31019  opnrebl2  31048  nn0prpw  31050  ordcmp  31178  findreccl  31184  nndivlub  31189  topdifinffinlem  31820  iooelexlt  31835  rdgeqoa  31843  wl-mo3t  31975  poimirlem2  32006  poimirlem23  32027  poimirlem28  32032  poimirlem29  32033  poimirlem31  32035  poimirlem32  32036  eqfnun  32112  sdclem2  32135  sdclem1  32136  prdsbnd2  32191  ismtyval  32196  rrnequiv  32231  exidreslem  32239  risci  32290  prtlem11  32502  prtlem15  32511  cvrat4  33079  lcfl6  35139  clcnvlem  36301  cnvrcl0  36303  cnvtrcl0  36304  iunrelexpmin1  36371  iunrelexpmin2  36375  aovmpt4g  38848  iccpartiltu  38881  iccpartgt  38886  iccpartgel  38888  zob  38908  gbepos  39004  pfxccatin12lem2  39112  f1ssf1  39167  incistruhgr  39325  upgredg2vtx  39392  upgredgpr  39393  uhgr2edg  39453  nbupgruvtxres  39644  cusgrfilem1  39681  1wlkres  39866  1wlkp1lem2  39870  pthdivtx  39922  pthdlem2lem  39953  eupth2lem3lem6  40145  ushguhg  40191  funcrngcsetc  40508  funcrngcsetcALT  40509  rhmsscrnghm  40536  funcringcsetc  40545  ellcoellss  40736  dignn0flhalflem2  40935  nn0sumshdiglemB  40939
  Copyright terms: Public domain W3C validator