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

Theorem syl5ibr 221
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 201 . 2  |-  ( ch 
->  ( th  <->  ps )
)
41, 3syl5ib 219 1  |-  ( ch 
->  ( ph  ->  ps ) )
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:  syl5ibrcom  222  biimprd  223  exdistrf  2048  pm2.61ne  2782  pm2.61neOLD  2783  unineq  3748  oteqex  4740  ordtri3  4914  limelon  4941  otel3xp  5035  elrnmpt1  5251  cnveqb  5462  cnveq0  5463  relcoi1  5536  ndmfv  5890  ffvresb  6052  isomin  6221  isofrlem  6224  caovord3d  6469  eldifpw  6596  ssonuni  6606  onsucuni2  6653  ordzsl  6664  tfindsg  6679  findsg  6711  oteqimp  6803  frxp  6893  poxp  6895  fnwelem  6898  suppss  6930  tfrlem11  7057  oacl  7185  omcl  7186  oecl  7187  oa0r  7188  om0r  7189  om1r  7192  oe1m  7194  oaordi  7195  oawordri  7199  oaass  7210  oarec  7211  omwordri  7221  odi  7228  omass  7229  oewordri  7241  oeworde  7242  oeordsuc  7243  oelim2  7244  oeoa  7246  oeoelem  7247  oeoe  7248  nnm0r  7259  nnacl  7260  nnacom  7266  nnaordi  7267  nnaass  7271  nndi  7272  nnmass  7273  nnmsucr  7274  nnmcom  7275  omabs  7296  brecop  7404  eceqoveq  7416  elpm2r  7436  map0g  7458  undifixp  7505  fundmen  7589  mapxpen  7683  mapunen  7686  php  7701  unxpdomlem2  7725  pssnn  7738  elfir  7875  wemapso2OLD  7977  wemapso2lem  7978  wdompwdom  8004  inf3lem1  8045  inf3lem3  8047  noinfepOLD  8077  cantnfval2  8088  cantnfp1lem3  8099  cantnfval2OLD  8118  cantnfp1lem3OLD  8125  r1sdom  8192  r1tr  8194  carden2a  8347  fidomtri2  8375  prdom2  8384  infxpenlem  8391  acndom  8432  fodomacn  8437  wdomfil  8442  alephon  8450  alephordi  8455  alephle  8469  alephfplem3  8487  dfac2a  8510  kmlem9  8538  cflm  8630  cfslb  8646  cfslbn  8647  infpssrlem3  8685  infpssrlem4  8686  fin23lem21  8719  fin23lem30  8722  isf34lem7  8759  isf34lem6  8760  fin67  8775  isfin7-2  8776  fin1a2lem7  8786  fin1a2lem10  8789  iundom2g  8915  konigthlem  8943  alephreg  8957  gchdomtri  9007  wunr1om  9097  tskr1om  9145  inar1  9153  grur1a  9197  indpi  9285  genpprecl  9379  genpnmax  9385  addcmpblnr  9446  recexsrlem  9480  map2psrpr  9487  ax1rid  9538  axpre-mulgt0  9545  ltle  9673  nnmulcl  10559  nnsub  10574  nn0sub  10846  nneo  10944  uzindOLD  10955  uz11  11104  xrltle  11355  xltnegi  11415  xrsupsslem  11498  xrinfmsslem  11499  xrub  11503  supxrunb1  11511  supxrunb2  11512  om2uzuzi  12028  uzrdgxfr  12045  seqcl2  12093  seqfveq2  12097  seqshft2  12101  seqsplit  12108  seqcaopr3  12110  seqf1olem2a  12113  seqid2  12121  seqhomo  12122  ser1const  12131  m1expcl2  12156  expadd  12176  expmul  12179  faclbnd  12336  hashmap  12459  hashfacen  12469  hashf1lem1  12470  hashf1lem2  12471  hashf1  12472  seqcoll  12478  wrdsymb0  12540  lsw0  12551  swrdvalodm2  12627  swrdvalodm  12628  wrd2ind  12666  swrdccatin12lem2  12677  swrdccatin1d  12687  repswccat  12720  repswcshw  12743  cshwcshid  12758  recan  13132  rexanre  13142  rlimcn2  13376  caurcvg2  13463  fsumiun  13598  efexp  13697  rpnnen2  13820  dvdstr  13878  alzdvds  13895  bitsinv1  13951  smu01lem  13994  smupval  13997  smueqlem  13999  smumullem  14001  seq1st  14059  prmdiveq  14175  odzdvds  14181  pythagtriplem2  14200  pcexp  14242  vdwlem13  14370  ramz  14402  elrestr  14684  xpsff1o  14823  subsubc  15080  clatl  15603  frmdgsum  15862  mulgneg2  15979  mulgnnass  15980  mhmmulg  15984  gsumwrev  16206  symgbas  16210  symgextf1lem  16250  symgfixelsi  16265  pmtrdifellem4  16310  sylow1lem1  16424  efgsfo  16563  efgred  16572  cyggexb  16704  gsumzres  16717  gsum2dlem2  16801  gsum2dOLD  16803  mulgass2  17048  lmodprop2d  17372  lspsnne2  17564  lspsneu  17569  assapropd  17775  mplcoe1  17926  mplcoe3  17927  mplcoe3OLD  17928  mplcoe5  17930  mplcoe2OLD  17932  ply1sclf1  18129  cnfldmulg  18249  cnfldexp  18250  zrhpsgnelbas  18425  mat1scmat  18836  restopn2  19472  cnpf2  19545  cmpfi  19702  txcn  19890  txlm  19912  xkoptsub  19918  xkopjcn  19920  ufildr  20195  cnflf  20266  fclsnei  20283  fclscmp  20294  ufilcmp  20296  cnfcf  20306  symgtgp  20363  isxms2  20714  met2ndc  20789  metustblOLD  20846  metustbl  20847  tngngp2  20929  clmmulg  21356  iscau4  21481  ovolunlem1a  21670  ovolicc2lem4  21694  volfiniun  21720  voliunlem1  21723  volsup  21729  dvnadd  22095  dvnres  22097  dvcobr  22112  ply1nzb  22286  plypf1  22372  dgrle  22403  coeaddlem  22408  dgrlt  22425  dvntaylp  22528  cxpmul2  22826  rlimcnp  23051  wilthlem2  23099  isnsqf  23165  musum  23223  chtub  23243  chpval2  23249  dchrisumlem1  23430  qabvexp  23567  ostthlem2  23569  axsegconlem1  23924  ax5seglem4  23939  ax5seglem5  23940  axlowdimlem15  23963  axcontlem2  23972  axcontlem4  23974  ushgrauhgra  24007  usgra2edg  24086  cusgrafilem1  24183  sizeusglecusglem1  24188  sizeusglecusg  24190  trliswlk  24245  2trllemF  24255  constr3lem6  24353  1conngra  24379  wlkiswwlk2lem4  24398  wwlknredwwlkn0  24431  wwlkextwrd  24432  wwlkextproplem1  24445  wwlkextprop  24448  clwlkisclwwlklem2a  24489  clwwlkf1  24500  erclwwlksym  24518  eleclclwwlknlem2  24522  erclwwlknsym  24530  el2wlkonot  24573  el2spthonot  24574  hashnbgravdg  24617  eupatrl  24672  frgra3vlem1  24704  3vfriswmgralem  24708  frconngra  24725  frgrawopreglem3  24751  frg2wot1  24762  2spotiundisj  24767  usg2spot2nb  24770  usgreg2spot  24772  extwwlkfablem2  24783  numclwwlkovf2ex  24791  extwwlkfab  24795  isexid2  25031  ismndo1  25050  rngo2  25094  rngoueqz  25136  sspval  25340  nmosetre  25383  nmobndseqi  25398  nmobndseqiOLD  25399  orthcom  25729  shsva  25942  shmodsi  26011  h1datomi  26203  nmopsetretALT  26486  nmfnsetre  26500  lnopcnbd  26659  pjclem4  26822  pj3si  26830  ssmd1  26934  atom1d  26976  chjatom  26980  atcvat4i  27020  cdj3lem2a  27059  cdj3lem3a  27062  disjunsn  27154  unitdivcld  27547  xrge0iifiso  27581  dya2iocuni  27922  facgam  28276  deranglem  28278  subfacp1lem6  28297  subfacval2  28299  cvmlift2lem12  28427  relexpsucr  28556  relexpsucl  28558  relexprel  28560  relexpdm  28561  relexprn  28562  relexpadd  28564  relexpindlem  28565  relexpind  28566  rtrclreclem.trans  28572  rtrclreclem.min  28573  dfrtrcl2  28574  rtrclind  28575  dfon2lem6  28825  rdgprc  28832  predpoirr  28882  predfrirr  28883  trpredlem1  28915  wfrlem14  28961  frrlem5e  29000  nodenselem8  29053  ifscgr  29299  btwncolinear1  29324  hfelhf  29443  ordcmp  29517  findreccl  29523  nndivlub  29528  wl-mo3t  29626  opnrebl2  29744  nn0prpw  29746  eqfnun  29843  sdclem2  29866  sdclem1  29867  prdsbnd2  29922  ismtyval  29927  rrnequiv  29962  exidreslem  29970  risci  30021  prtlem11  30239  prtlem15  30248  aovmpt4g  31781  f1vrnfibi  31808  ushguhg  31866  mgmplusgiop  31961  sgrpplusgaop  31962  ellcoellss  32135  bnj168  32883  bnj535  33045  bnj590  33065  bnj594  33067  bnj938  33092  bnj1118  33137  bnj1128  33143  cvrat4  34257  lcfl6  36315
  Copyright terms: Public domain W3C validator