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  2025  pm2.61ne  2710  unineq  3621  oteqex  4605  ordtri3  4776  limelon  4803  elrnmpt1  5109  cnveqb  5314  cnveq0  5315  relcoi1  5387  ndmfv  5735  ffvresb  5895  isomin  6049  isofrlem  6052  caovord3d  6294  eldifpw  6409  ssonuni  6419  onsucuni2  6466  ordzsl  6477  tfindsg  6492  findsg  6524  frxp  6703  poxp  6705  fnwelem  6708  suppss  6740  tfrlem11  6868  oacl  6996  omcl  6997  oecl  6998  oa0r  6999  om0r  7000  om1r  7003  oe1m  7005  oaordi  7006  oawordri  7010  oaass  7021  oarec  7022  omwordri  7032  odi  7039  omass  7040  oewordri  7052  oeworde  7053  oeordsuc  7054  oelim2  7055  oeoa  7057  oeoelem  7058  oeoe  7059  nnm0r  7070  nnacl  7071  nnacom  7077  nnaordi  7078  nnaass  7082  nndi  7083  nnmass  7084  nnmsucr  7085  nnmcom  7086  omabs  7107  brecop  7214  eceqoveq  7226  elpm2r  7251  map0g  7273  undifixp  7320  fundmen  7404  mapxpen  7498  mapunen  7501  php  7516  unxpdomlem2  7539  pssnn  7552  elfir  7686  wemapso2OLD  7787  wemapso2lem  7788  wdompwdom  7814  inf3lem1  7855  inf3lem3  7857  noinfepOLD  7887  cantnfval2  7898  cantnfp1lem3  7909  cantnfval2OLD  7928  cantnfp1lem3OLD  7935  r1sdom  8002  r1tr  8004  carden2a  8157  fidomtri2  8185  prdom2  8194  infxpenlem  8201  acndom  8242  fodomacn  8247  wdomfil  8252  alephon  8260  alephordi  8265  alephle  8279  alephfplem3  8297  dfac2a  8320  kmlem9  8348  cflm  8440  cfslb  8456  cfslbn  8457  infpssrlem3  8495  infpssrlem4  8496  fin23lem21  8529  fin23lem30  8532  isf34lem7  8569  isf34lem6  8570  fin67  8585  isfin7-2  8586  fin1a2lem7  8596  fin1a2lem10  8599  iundom2g  8725  konigthlem  8753  alephreg  8767  gchdomtri  8817  wunr1om  8907  tskr1om  8955  inar1  8963  grur1a  9007  indpi  9097  genpprecl  9191  genpnmax  9197  addcmpblnr  9260  recexsrlem  9291  map2psrpr  9298  ax1rid  9349  axpre-mulgt0  9356  ltle  9484  nnmulcl  10366  nnsub  10381  nn0sub  10651  nneo  10746  uzindOLD  10757  uz11  10904  xrltle  11147  xltnegi  11207  xrsupsslem  11290  xrinfmsslem  11291  xrub  11295  supxrunb1  11303  supxrunb2  11304  om2uzuzi  11793  uzrdgxfr  11810  seqcl2  11845  seqfveq2  11849  seqshft2  11853  seqsplit  11860  seqcaopr3  11862  seqf1olem2a  11865  seqid2  11873  seqhomo  11874  ser1const  11883  m1expcl2  11908  expadd  11927  expmul  11930  faclbnd  12087  hashmap  12218  hashfacen  12228  hashf1lem1  12229  hashf1lem2  12230  hashf1  12231  seqcoll  12237  wrdsymb0  12280  lsw0  12288  swrdvalodm2  12354  swrdvalodm  12355  wrd2ind  12393  swrdccatin12lem2  12401  swrdccatin1d  12411  repswccat  12444  repswcshw  12467  recan  12845  rexanre  12855  rlimcn2  13089  caurcvg2  13176  fsumiun  13305  efexp  13406  rpnnen2  13529  dvdstr  13587  alzdvds  13604  bitsinv1  13659  smu01lem  13702  smupval  13705  smueqlem  13707  smumullem  13709  seq1st  13767  prmdiveq  13882  odzdvds  13888  pythagtriplem2  13905  pcexp  13947  vdwlem13  14075  ramz  14107  elrestr  14388  xpsff1o  14527  subsubc  14784  clatl  15307  frmdgsum  15561  mulgneg2  15675  mulgnnass  15676  mhmmulg  15680  gsumwrev  15902  symgbas  15906  symgextf1lem  15946  symgfixelsi  15961  pmtrdifellem4  16006  sylow1lem1  16118  efgsfo  16257  efgred  16266  cyggexb  16396  gsumzres  16409  gsum2dlem2  16484  gsum2dOLD  16486  mulgass2  16714  lmodprop2d  17029  lspsnne2  17221  lspsneu  17226  assapropd  17420  mplcoe1  17566  mplcoe3  17567  mplcoe3OLD  17568  mplcoe5  17570  mplcoe2OLD  17572  ply1sclf1  17763  cnfldmulg  17870  cnfldexp  17871  zrhpsgnelbas  18046  restopn2  18803  cnpf2  18876  cmpfi  19033  txcn  19221  txlm  19243  xkoptsub  19249  xkopjcn  19251  ufildr  19526  cnflf  19597  fclsnei  19614  fclscmp  19625  ufilcmp  19627  cnfcf  19637  symgtgp  19694  isxms2  20045  met2ndc  20120  metustblOLD  20177  metustbl  20178  tngngp2  20260  clmmulg  20687  iscau4  20812  ovolunlem1a  21001  ovolicc2lem4  21025  volfiniun  21050  voliunlem1  21053  volsup  21059  dvnadd  21425  dvnres  21427  dvcobr  21442  ply1nzb  21616  plypf1  21702  dgrle  21733  coeaddlem  21738  dgrlt  21755  dvntaylp  21858  cxpmul2  22156  rlimcnp  22381  wilthlem2  22429  isnsqf  22495  musum  22553  chtub  22573  chpval2  22579  dchrisumlem1  22760  qabvexp  22897  ostthlem2  22899  axsegconlem1  23185  ax5seglem4  23200  ax5seglem5  23201  axlowdimlem15  23224  axcontlem2  23233  axcontlem4  23235  usgra2edg  23323  cusgrafilem1  23409  sizeusglecusglem1  23414  sizeusglecusg  23416  trliswlk  23460  2trllemF  23470  constr3lem6  23557  1conngra  23583  hashnbgravdg  23603  eupatrl  23611  isexid2  23834  ismndo1  23853  rngo2  23897  rngoueqz  23939  sspval  24143  nmosetre  24186  nmobndseqi  24201  nmobndseqiOLD  24202  orthcom  24532  shsva  24745  shmodsi  24814  h1datomi  25006  nmopsetretALT  25289  nmfnsetre  25303  lnopcnbd  25462  pjclem4  25625  pj3si  25633  ssmd1  25737  atom1d  25779  chjatom  25783  atcvat4i  25823  cdj3lem2a  25862  cdj3lem3a  25865  disjunsn  25958  unitdivcld  26353  xrge0iifiso  26387  dya2iocuni  26720  facgam  27074  deranglem  27076  subfacp1lem6  27095  subfacval2  27097  cvmlift2lem12  27225  relexpsucr  27354  relexpsucl  27356  relexprel  27358  relexpdm  27359  relexprn  27360  relexpadd  27362  relexpindlem  27363  relexpind  27364  rtrclreclem.trans  27370  rtrclreclem.min  27371  dfrtrcl2  27372  rtrclind  27373  dfon2lem6  27623  rdgprc  27630  predpoirr  27680  predfrirr  27681  trpredlem1  27713  wfrlem14  27759  frrlem5e  27798  nodenselem8  27851  ifscgr  28097  btwncolinear1  28122  hfelhf  28241  ordcmp  28315  findreccl  28321  nndivlub  28326  wl-mo3t  28423  opnrebl2  28542  nn0prpw  28544  eqfnun  28641  sdclem2  28664  sdclem1  28665  prdsbnd2  28720  ismtyval  28725  rrnequiv  28760  exidreslem  28768  risci  28819  prtlem11  29037  prtlem15  29046  aovmpt4g  30133  otel3xp  30154  oteqimp  30155  wlkiswwlk2lem4  30354  wwlknredwwlkn0  30385  wwlkextwrd  30386  el2wlkonot  30414  el2spthonot  30415  clwlkisclwwlklem2a  30473  clwwlkf1  30484  erclwwlksym0  30504  erclwwlksym  30510  eleclclwwlknlem2  30517  erclwwlknsym  30526  wwlkextproplem1  30586  wwlkextprop  30589  frgra3vlem1  30618  3vfriswmgralem  30622  frconngra  30639  frgrawopreglem3  30665  frg2wot1  30676  2spotiundisj  30681  usg2spot2nb  30684  usgreg2spot  30686  extwwlkfablem2  30697  numclwwlkovf2ex  30705  extwwlkfab  30709  ellcoellss  30966  bnj168  31817  bnj535  31979  bnj590  31999  bnj594  32001  bnj938  32026  bnj1118  32071  bnj1128  32077  cvrat4  33183  lcfl6  35241
  Copyright terms: Public domain W3C validator