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

Theorem syl5ibr 225
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 205 . 2  |-  ( ch 
->  ( th  <->  ps )
)
41, 3syl5ib 223 1  |-  ( ch 
->  ( ph  ->  ps ) )
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:  syl5ibrcom  226  biimprd  227  exdistrf  2167  pm2.61ne  2709  unineq  3693  elpreqprlem  4160  oteqex  4694  otel3xp  4870  elrnmpt1  5083  cnveqb  5291  cnveq0  5292  relcoi1OLD  5365  predpoirr  5408  predfrirr  5409  ordtri3  5459  limelon  5486  ndmfv  5889  ffvresb  6054  isomin  6228  isofrlem  6231  caovord3d  6479  eldifpw  6603  ssonuni  6613  onsucuni2  6661  ordzsl  6672  tfindsg  6687  findsg  6720  oteqimp  6812  frxp  6906  poxp  6908  fnwelem  6911  suppss  6945  wfrlem14  7049  tfrlem11  7106  oacl  7237  omcl  7238  oecl  7239  oa0r  7240  om0r  7241  om1r  7244  oe1m  7246  oaordi  7247  oawordri  7251  oaass  7262  oarec  7263  omwordri  7273  odi  7280  omass  7281  oewordri  7293  oeworde  7294  oeordsuc  7295  oelim2  7296  oeoa  7298  oeoelem  7299  oeoe  7300  nnm0r  7311  nnacl  7312  nnacom  7318  nnaordi  7319  nnaass  7323  nndi  7324  nnmass  7325  nnmsucr  7326  nnmcom  7327  omabs  7348  brecop  7456  eceqoveq  7468  elpm2r  7489  map0g  7511  undifixp  7558  fundmen  7643  mapxpen  7738  mapunen  7741  php  7756  unxpdomlem2  7777  pssnn  7790  f1vrnfibi  7859  elfir  7929  wemapso2lem  8067  wdompwdom  8093  inf3lem1  8133  inf3lem3  8135  cantnfval2  8174  cantnfp1lem3  8185  r1sdom  8245  r1tr  8247  carden2a  8400  fidomtri2  8428  prdom2  8437  infxpenlem  8444  acndom  8482  fodomacn  8487  wdomfil  8492  alephon  8500  alephordi  8505  alephle  8519  alephfplem3  8537  dfac2a  8560  kmlem9  8588  cflm  8680  cfslb  8696  cfslbn  8697  infpssrlem3  8735  infpssrlem4  8736  fin23lem21  8769  fin23lem30  8772  isf34lem7  8809  isf34lem6  8810  fin67  8825  isfin7-2  8826  fin1a2lem7  8836  fin1a2lem10  8839  iundom2g  8965  konigthlem  8993  alephreg  9007  gchdomtri  9054  wunr1om  9144  tskr1om  9192  inar1  9200  grur1a  9244  indpi  9332  genpprecl  9426  genpnmax  9432  addcmpblnr  9493  recexsrlem  9527  map2psrpr  9534  ax1rid  9585  axpre-mulgt0  9592  ltle  9722  nnmulcl  10632  nnsub  10648  nn0sub  10920  nneo  11019  uz11  11181  xrltle  11448  xltnegi  11509  xrsupsslem  11592  xrinfmsslem  11593  xrub  11597  supxrunb1  11605  supxrunb2  11606  om2uzuzi  12163  uzrdgxfr  12180  seqcl2  12231  seqfveq2  12235  seqshft2  12239  seqsplit  12246  seqcaopr3  12248  seqf1olem2a  12251  seqid2  12259  seqhomo  12260  ser1const  12269  m1expcl2  12294  expadd  12314  expmul  12317  faclbnd  12475  hashmap  12607  hashfacen  12617  hashf1lem1  12618  hashf1lem2  12619  hashf1  12620  seqcoll  12627  wrdsymb0  12701  swrdnd2  12789  wrd2ind  12834  swrdccatin12lem2  12845  swrdccatin1d  12855  repswccat  12888  repswcshw  12911  cshwcshid  12926  rtrclreclem3  13123  rtrclreclem4  13124  dfrtrcl2  13125  relexpindlem  13126  relexpind  13127  rtrclind  13128  recan  13399  rexanre  13409  rlimcn2  13654  caurcvg2  13744  fsumiun  13881  efexp  14155  rpnnen2  14278  dvdstr  14337  alzdvds  14355  bitsinv1  14416  smu01lem  14459  smupval  14462  smueqlem  14464  smumullem  14466  seq1st  14530  lcmfunsnlem2lem1  14611  lcmfunsnlem2lem2  14612  prmdiveq  14734  odzdvds  14740  odzdvdsOLD  14746  pythagtriplem2  14767  pcexp  14809  vdwlem13  14943  ramz  14983  prmolefac  15004  prmorlefacOLD  15018  elrestr  15327  xpsff1o  15474  subsubc  15758  clatl  16362  frmdgsum  16646  mulgneg2  16785  mulgnnass  16786  mhmmulg  16790  gsumwrev  17017  symgbas  17021  symgextf1lem  17061  symgfixelsi  17076  pmtrdifellem4  17120  sylow1lem1  17250  efgsfo  17389  efgred  17398  cyggexb  17533  gsumzres  17543  gsum2dlem2  17603  mulgass2  17829  lmodprop2d  18150  lspsnne2  18341  lspsneu  18346  assapropd  18551  mplcoe1  18689  mplcoe3  18690  mplcoe5  18692  ply1sclf1  18882  cnfldmulg  19000  cnfldexp  19001  zrhpsgnelbas  19162  mat1scmat  19564  restopn2  20193  cnpf2  20266  cmpfi  20423  txcn  20641  txlm  20663  xkoptsub  20669  xkopjcn  20671  ufildr  20946  cnflf  21017  fclsnei  21034  fclscmp  21045  ufilcmp  21047  cnfcf  21057  symgtgp  21116  isxms2  21463  met2ndc  21538  metustbl  21581  tngngp2  21660  clmmulg  22124  iscau4  22249  ovolunlem1a  22449  ovolicc2lem4OLD  22473  ovolicc2lem4  22474  volfiniun  22500  voliunlem1  22503  volsup  22509  dvnadd  22883  dvnres  22885  dvcobr  22900  ply1nzb  23071  plypf1  23166  dgrle  23197  coeaddlem  23203  dgrlt  23220  dvntaylp  23326  cxpmul2  23634  rlimcnp  23891  facgam  23991  wilthlem2  23994  isnsqf  24062  musum  24120  chtub  24140  chpval2  24146  dchrisumlem1  24327  qabvexp  24464  ostthlem2  24466  axsegconlem1  24947  ax5seglem4  24962  ax5seglem5  24963  axlowdimlem15  24986  axcontlem2  24995  axcontlem4  24997  ushgrauhgra  25030  usgra2edg  25109  cusgrafilem1  25207  sizeusglecusglem1  25212  sizeusglecusg  25214  trliswlk  25269  2trllemF  25279  constr3lem6  25377  1conngra  25403  wlkiswwlk2lem4  25422  wwlknredwwlkn0  25455  wwlkextwrd  25456  wwlkextproplem1  25469  wwlkextprop  25472  clwlkisclwwlklem2a  25513  clwwlkf1  25524  erclwwlksym  25542  eleclclwwlknlem2  25546  erclwwlknsym  25554  el2wlkonot  25597  el2spthonot  25598  hashnbgravdg  25641  eupatrl  25696  frgra3vlem1  25728  3vfriswmgralem  25732  frconngra  25749  frgrawopreglem3  25774  frg2wot1  25785  2spotiundisj  25790  usg2spot2nb  25793  usgreg2spot  25795  extwwlkfablem2  25806  numclwwlkovf2ex  25814  extwwlkfab  25818  isexid2  26053  ismndo1  26072  rngo2  26116  rngoueqz  26158  sspval  26362  nmosetre  26405  nmobndseqi  26420  nmobndseqiALT  26421  orthcom  26761  shsva  26973  shmodsi  27042  h1datomi  27234  nmopsetretALT  27516  nmfnsetre  27530  lnopcnbd  27689  pjclem4  27852  pj3si  27860  ssmd1  27964  atom1d  28006  chjatom  28010  atcvat4i  28050  cdj3lem2a  28089  cdj3lem3a  28092  disjunsn  28204  unitdivcld  28707  xrge0iifiso  28741  dya2iocuni  29105  bnj168  29538  bnj535  29701  bnj590  29721  bnj594  29723  bnj938  29748  bnj1118  29793  bnj1128  29799  deranglem  29889  subfacp1lem6  29908  subfacval2  29910  cvmlift2lem12  30037  mrsubvrs  30160  msrrcl  30181  mclsax  30207  dfon2lem6  30434  rdgprc  30441  trpredlem1  30468  frrlem5e  30522  nodenselem8  30577  ifscgr  30811  btwncolinear1  30836  hfelhf  30948  opnrebl2  30977  nn0prpw  30979  ordcmp  31107  findreccl  31113  nndivlub  31118  topdifinffinlem  31750  iooelexlt  31765  rdgeqoa  31773  wl-mo3t  31905  poimirlem2  31942  poimirlem23  31963  poimirlem28  31968  poimirlem29  31969  poimirlem31  31971  poimirlem32  31972  eqfnun  32048  sdclem2  32071  sdclem1  32072  prdsbnd2  32127  ismtyval  32132  rrnequiv  32167  exidreslem  32175  risci  32226  prtlem11  32438  prtlem15  32447  cvrat4  33008  lcfl6  35068  clcnvlem  36230  cnvrcl0  36232  cnvtrcl0  36233  iunrelexpmin1  36300  iunrelexpmin2  36304  aovmpt4g  38703  iccpartiltu  38736  iccpartgt  38741  iccpartgel  38743  zob  38763  gbepos  38859  pfxccatin12lem2  38965  f1ssf1  39021  incistruhgr  39171  upgredg2vtx  39231  upgredgpr  39232  usgr2edg  39291  nbupgruvtxres  39480  cusgrfilem1  39516  ushguhg  39736  funcrngcsetc  40053  funcrngcsetcALT  40054  rhmsscrnghm  40081  funcringcsetc  40090  ellcoellss  40281  dignn0flhalflem2  40480  nn0sumshdiglemB  40484
  Copyright terms: Public domain W3C validator