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

Theorem syl5ibr 213
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 193 . 2  |-  ( ch 
->  ( th  <->  ps )
)
41, 3syl5ib 211 1  |-  ( ch 
->  ( ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  syl5ibrcom  214  biimprd  215  dvelimvOLD  2028  exdistrf  2062  pm2.61ne  2673  unineq  3583  oteqex  4441  ordtri3  4609  limelon  4636  eldifpw  4747  ssonuni  4759  onsucuni2  4806  ordzsl  4817  tfindsg  4832  findsg  4864  elrnmpt1  5111  cnveqb  5318  cnveq0  5319  relcoi1  5390  ndmfv  5747  ffvresb  5892  isomin  6049  isofrlem  6052  caovord3d  6249  frxp  6448  poxp  6450  fnwelem  6453  tfrlem1  6628  tfrlem11  6641  oacl  6771  omcl  6772  oecl  6773  oa0r  6774  om0r  6775  om1r  6778  oe1m  6780  oaordi  6781  oawordri  6785  oaass  6796  oarec  6797  omwordri  6807  odi  6814  omass  6815  oewordri  6827  oeworde  6828  oeordsuc  6829  oelim2  6830  oeoa  6832  oeoelem  6833  oeoe  6834  nnm0r  6845  nnacl  6846  nnacom  6852  nnaordi  6853  nnaass  6857  nndi  6858  nnmass  6859  nnmsucr  6860  nnmcom  6861  omabs  6882  brecop  6989  eceqoveq  7001  elpm2r  7026  map0g  7045  undifixp  7090  fundmen  7172  mapxpen  7265  mapunen  7268  php  7283  unxpdomlem2  7306  pssnn  7319  elfir  7412  wemapso2  7513  wdompwdom  7538  inf3lem1  7575  inf3lem3  7577  noinfepOLD  7607  cantnfval2  7616  cantnfp1lem3  7628  r1sdom  7692  r1tr  7694  carden2a  7845  fidomtri2  7873  prdom2  7882  infxpenlem  7887  acndom  7924  fodomacn  7929  wdomfil  7934  alephon  7942  alephordi  7947  alephle  7961  alephfplem3  7979  dfac2a  8002  kmlem9  8030  cflm  8122  cfslb  8138  cfslbn  8139  infpssrlem3  8177  infpssrlem4  8178  fin23lem21  8211  fin23lem30  8214  isf34lem7  8251  isf34lem6  8252  fin67  8267  isfin7-2  8268  fin1a2lem7  8278  fin1a2lem10  8281  iundom2g  8407  konigthlem  8435  alephreg  8449  gchdomtri  8496  wunr1om  8586  tskr1om  8634  inar1  8642  grur1a  8686  indpi  8776  genpprecl  8870  genpnmax  8876  addcmpblnr  8939  recexsrlem  8970  map2psrpr  8977  ax1rid  9028  axpre-mulgt0  9035  ltle  9155  nnmulcl  10015  nnsub  10030  nn0sub  10262  nneo  10345  uzindOLD  10356  uz11  10500  xrltle  10734  xltnegi  10794  xrsupsslem  10877  xrinfmsslem  10878  xrub  10882  supxrunb1  10890  supxrunb2  10891  om2uzuzi  11281  uzrdgxfr  11298  seqcl2  11333  seqfveq2  11337  seqshft2  11341  seqsplit  11348  seqcaopr3  11350  seqf1olem2a  11353  seqid2  11361  seqhomo  11362  ser1const  11371  m1expcl2  11395  expadd  11414  expmul  11417  faclbnd  11573  hashmap  11690  hashfacen  11695  hashf1lem1  11696  hashf1lem2  11697  hashf1  11698  seqcoll  11704  recan  12132  rexanre  12142  rlimcn2  12376  caurcvg2  12463  fsumiun  12592  efexp  12694  rpnnen2  12817  dvdstr  12875  alzdvds  12891  bitsinv1  12946  smu01lem  12989  smupval  12992  smueqlem  12994  smumullem  12996  seq1st  13054  prmdiveq  13167  odzdvds  13173  pythagtriplem2  13183  pcexp  13225  vdwlem13  13353  ramz  13385  elrestr  13648  xpsff1o  13785  subsubc  14042  frmdgsum  14799  mulgneg2  14909  mulgnnass  14910  mhmmulg  14914  symgbas  15087  gsumwrev  15154  sylow1lem1  15224  efgsfo  15363  efgred  15372  cyggexb  15500  gsum2d  15538  mulgass2  15702  lmodprop2d  15998  lspsnne2  16182  lspsneu  16187  assapropd  16378  mplcoe1  16520  mplcoe3  16521  mplcoe2  16522  ply1sclf1  16672  cnfldmulg  16725  cnfldexp  16726  restopn2  17233  cnpf2  17306  cmpfi  17463  txcn  17650  txlm  17672  xkoptsub  17678  xkopjcn  17680  ufildr  17955  cnflf  18026  fclsnei  18043  fclscmp  18054  ufilcmp  18056  cnfcf  18066  symgtgp  18123  isxms2  18470  met2ndc  18545  metustblOLD  18602  metustbl  18603  tngngp2  18685  clmmulg  19110  iscau4  19224  ovolunlem1a  19384  ovolicc2lem4  19408  volfiniun  19433  voliunlem1  19436  volsup  19442  dvnadd  19807  dvnres  19809  dvcobr  19824  ply1nzb  20037  plypf1  20123  dgrle  20154  coeaddlem  20159  dgrlt  20176  dvntaylp  20279  cxpmul2  20572  rlimcnp  20796  wilthlem2  20844  isnsqf  20910  musum  20968  chtub  20988  chpval2  20994  dchrisumlem1  21175  qabvexp  21312  ostthlem2  21314  usgra2edg  21394  cusgrafilem1  21480  sizeusglecusglem1  21485  sizeusglecusg  21487  trliswlk  21531  2trllemF  21541  constr3lem6  21628  1conngra  21654  hashnbgravdg  21674  eupatrl  21682  isexid2  21905  ismndo1  21924  rngo2  21968  rngoueqz  22010  sspval  22214  nmosetre  22257  nmobndseqi  22272  nmobndseqiOLD  22273  orthcom  22602  shsva  22814  shmodsi  22883  h1datomi  23075  nmopsetretALT  23358  nmfnsetre  23372  lnopcnbd  23531  pjclem4  23694  pj3si  23702  ssmd1  23806  atom1d  23848  chjatom  23852  atcvat4i  23892  cdj3lem2a  23931  cdj3lem3a  23934  unitdivcld  24291  xrge0iifiso  24313  dya2iocuni  24625  facgam  24842  deranglem  24844  subfacp1lem6  24863  subfacval2  24865  cvmlift2lem12  24993  relexpsucr  25122  relexpsucl  25124  relexprel  25126  relexpdm  25127  relexprn  25128  relexpadd  25130  relexpindlem  25131  relexpind  25132  rtrclreclem.trans  25138  rtrclreclem.min  25139  dfrtrcl2  25140  rtrclind  25141  dfon2lem6  25407  rdgprc  25414  predpoirr  25464  predfrirr  25465  trpredlem1  25497  wfrlem14  25543  frrlem5e  25582  nodenselem8  25635  axsegconlem1  25848  ax5seglem4  25863  ax5seglem5  25864  axlowdimlem15  25887  axcontlem2  25896  axcontlem4  25898  ifscgr  25970  btwncolinear1  25995  hfelhf  26114  ordcmp  26189  findreccl  26195  nndivlub  26200  opnrebl2  26305  nn0prpw  26307  eqfnun  26404  sdclem2  26427  sdclem1  26428  prdsbnd2  26485  ismtyval  26490  rrnequiv  26525  exidreslem  26533  risci  26584  prtlem11  26696  prtlem15  26705  aovmpt4g  28022  otel3xp  28042  oteqimp  28043  wrdsymb0  28137  swrdvalodm2  28150  swrdvalodm  28151  swrdccatin12lem3  28168  swrdccatin2d  28177  2cshwmod  28213  lswrd0  28217  el2wlkonot  28279  el2spthonot  28280  frgra3vlem1  28317  3vfriswmgralem  28321  frconngra  28338  frgrawopreglem3  28362  frg2wot1  28373  2spotiundisj  28378  usg2spot2nb  28381  usgreg2spot  28383  bnj168  29024  bnj535  29188  bnj590  29208  bnj594  29210  bnj938  29235  bnj1118  29280  bnj1128  29286  dvelimvNEW7  29389  cvrat4  30167  lcfl6  32225
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 178
  Copyright terms: Public domain W3C validator