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

Theorem syl5bb 249
Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl5bb.1  |-  ( ph  <->  ps )
syl5bb.2  |-  ( ch 
->  ( ps  <->  th )
)
Assertion
Ref Expression
syl5bb  |-  ( ch 
->  ( ph  <->  th )
)

Proof of Theorem syl5bb
StepHypRef Expression
1 syl5bb.1 . . 3  |-  ( ph  <->  ps )
21a1i 11 . 2  |-  ( ch 
->  ( ph  <->  ps )
)
3 syl5bb.2 . 2  |-  ( ch 
->  ( ps  <->  th )
)
42, 3bitrd 245 1  |-  ( ch 
->  ( ph  <->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  syl5rbb  250  syl5bbr  251  3bitr4g  280  imim21b  357  cad0  1409  had1  1411  ax11wdemo  1738  ax12olem6OLD  2016  sbcom  2164  abbi  2545  necon3abid  2631  necon3bid  2633  necon1abid  2651  r19.21t  2783  ceqsralt  2971  ceqsrexv  3061  ceqsrex2v  3063  elab2g  3076  elrabf  3083  eueq2  3100  eqreu  3118  reu8  3122  ru  3152  sbcralt  3225  csbnestgf  3291  disjpss  3670  ralprg  3849  rexprg  3850  difsn  3925  opthpr  3968  ralunsn  3995  dfiin2g  4116  iunxsng  4161  elpwuni  4170  disjxun  4202  pwnss  4357  opelopabt  4459  opelopabga  4460  brabga  4461  dfid3  4491  frirr  4551  wereu2  4571  ordtri4  4610  oneqmini  4624  elsucg  4640  elsuc2g  4641  dfwe2  4754  ssonprc  4764  ordpwsuc  4787  dfom2  4839  brab2a  4919  opeliunxp  4921  posn  4938  sosn  4939  frsn  4940  brab2ga  4943  opbrop  4947  elrnmpt1  5111  elrnmptg  5112  eliniseg2  5236  poleloe  5260  cnvpo  5402  dffun8  5472  fncnv  5507  fununi  5509  fnssresb  5549  fnimaeq0  5558  funcocnv2  5692  dffn5  5764  funimass4  5769  fnsnfv  5778  dmfco  5789  fndmdif  5826  fvimacnvi  5836  fvimacnvALT  5841  unpreima  5848  respreima  5851  fmptco  5893  fressnfv  5912  fnsuppres  5944  elunirnALT  5992  dff13  5996  fliftel  6023  isoini  6050  f1oiso  6063  f1oweALT  6066  eloprabga  6152  resoprab2  6159  ralrnmpt2  6176  ovid  6182  ov  6185  ovg  6204  ofrfval2  6315  fmpt2x  6409  ovmptss  6420  1stconst  6427  2ndconst  6428  isprmpt2  6469  brtpos2  6477  dfsmo2  6601  tfrlem1  6628  rdglim2  6682  seqomlem2  6700  omeu  6820  oeeui  6837  brdifun  6924  eqerlem  6929  brecop  6989  erovlem  6992  eceqoveq  7001  mapsn  7047  mptelixpg  7091  map1  7177  xpsnen  7184  xpdom2  7195  omxpenlem  7201  xpf1o  7261  mapunen  7268  onfin  7289  fimaxg  7346  fodomfib  7378  fofinf1o  7379  fipreima  7404  supub  7456  ordtypecbv  7478  ordtypelem3  7481  ordtypelem9  7487  hartogslem1  7503  wofib  7506  wemapso2lem  7511  wemapso2  7513  noinfep  7606  noinfepOLD  7607  cantnf  7641  rankbnd2  7787  domtri2  7868  infxpenc2  7895  fseqdom  7899  acni2  7919  dfac9  8008  cfeq0  8128  cfsuc  8129  cflim3  8134  cfslb  8138  cofsmo  8141  enfin2i  8193  isfin3ds  8201  isf33lem  8238  fin1a2lem5  8276  axdc2lem  8320  zorn2g  8375  fodomb  8396  brdom7disj  8401  brdom6disj  8402  iundom2g  8407  cfpwsdom  8451  elgch  8489  fpwwe2cbv  8497  fpwwecbv  8511  pwfseqlem3  8527  pwfseqlem4a  8528  pwfseqlem4  8529  ltpiord  8756  nlt1pi  8775  nqereu  8798  addclprlem1  8885  1idpr  8898  reclem3pr  8918  ltsosr  8961  map2psrpr  8977  supsrlem  8978  axrrecex  9030  xrlenlt  9135  eqlei2  9176  addsubeq4  9312  renegcli  9354  lesub0  9536  wloglei  9551  conjmul  9723  rereccl  9724  infm3  9959  supmul1  9965  supmullem1  9966  supmullem2  9967  supmul  9968  creui  9987  nndiv  10032  elznn0  10288  prime  10342  eqreznegel  10553  zsupss  10557  rebtwnz  10565  ltxr  10707  elixx3g  10921  ixxun  10924  ioo0  10933  ico0  10954  ioc0  10955  icc0  10956  difreicc  11020  iccf1o  11031  elfz2  11042  fzn  11063  fznn  11107  fzshftral  11126  fzosplitsni  11188  om2uzisoi  11286  sq11i  11464  hashsdom  11647  brfi1uzind  11707  wrdval  11722  s2f1o  11855  cjreb  11920  rexfiuz  12143  cau3lem  12150  rlim2  12282  ello12  12302  ello1mpt  12307  elo12  12313  o1lo1  12323  lo1resb  12350  o1resb  12352  o1compt  12373  caucvgb  12465  mertens  12655  ruclem12  12832  divides  12846  odd2np1  12900  oddm1even  12901  sadadd2lem2  12954  gcdcllem2  13004  bezoutlem2  13031  bezoutlem3  13032  bezoutlem4  13033  isprm2  13079  isprm3  13080  prmreclem2  13277  prmreclem5  13280  prmreclem6  13281  4sqlem2  13309  4sqlem12  13316  vdwmc  13338  vdwpc  13340  vdwlem6  13346  vdwlem10  13350  vdwnn  13358  ramval  13368  0ram  13380  prdsleval  13691  pwsle  13706  imasleval  13758  xpsfrnel2  13782  xpsle  13798  isacs2  13870  mreacs  13875  acsfn  13876  iscatd2  13898  catpropd  13927  isssc  14012  evlfcl  14311  uncfcurf  14328  pltval  14409  lubid  14431  tosso  14457  oduleg  14551  oduclatb  14563  isipodrs  14579  odudlatb  14614  spwpr2  14652  spwex  14653  gsumvalx  14766  grplmulf1o  14857  grplactcnv  14879  elnmz  14971  eqgid  14984  isghm  14998  ghmeqker  15024  resscntz  15122  odmulgeq  15185  sylow3lem3  15255  sylow3lem6  15258  efgval2  15348  efgsdm  15354  efgrelexlema  15373  efgcpbllemb  15379  iscyggen2  15483  cyggenod  15486  eldprd  15554  dprdf11  15573  dprddisj2  15589  pgpfac1lem2  15625  pgpfac1  15630  drngid2  15843  issubrg  15860  islmod  15946  aspval2  16397  psrbag  16423  zndvds  16822  znleval  16827  iunocv  16900  pjfval2  16928  pjdm2  16930  istopg  16960  istpsOLD  16977  basgen2  17046  isclo  17143  mretopd  17148  isnei  17159  isperf3  17209  restdis  17234  neitr  17236  restcls  17237  restlp  17239  restperf  17240  iscn  17291  iscnp  17293  lmbr2  17315  lmbrf  17316  ordtt1  17435  cmpsub  17455  hauscmplem  17461  cmpfi  17463  bwth  17465  dfcon2  17474  1stcelcls  17516  1stccn  17518  nllyi  17530  subislly  17536  elkgen  17560  ptpjpre1  17595  ptuni2  17600  ptclsg  17639  ptcnplem  17645  txcn  17650  hausdiag  17669  txhaus  17671  txkgen  17676  xkoptsub  17678  cnmpt21  17695  elqtop  17721  tgqtop  17736  r0cld  17762  elfg  17895  fbasrn  17908  trfil2  17911  trfil3  17912  fin1aufil  17956  elfm2  17972  elfm3  17974  flimopn  17999  fbflim  18000  flfnei  18015  flftg  18020  cnpflf2  18024  txflf  18030  fclsbas  18045  alexsubALTlem4  18073  cnextfvval  18088  snclseqg  18137  tgphaus  18138  tsmsfbas  18149  tsmssubm  18164  utopsnneip  18270  prdsxmetlem  18390  imasdsf1olem  18395  xpsdsval  18403  blres  18453  isxms2  18470  metcnp  18563  txmetcnp  18569  txmetcn  18570  metustelOLD  18573  metustel  18574  metuel2  18601  dscopn  18613  isngp4  18650  cnblcld  18801  metnrmlem1a  18880  icoopnst  18956  iocopnst  18957  elpi1  19062  lmmbr2  19204  cfil3i  19214  caucfil  19228  iscmet3  19238  lmclim  19247  metcld2  19251  bcthlem4  19272  minveclem3b  19321  minveclem6  19327  minveclem7  19328  ivthle  19345  ivthle2  19346  evthicc2  19349  ovolfioo  19356  ovolficc  19357  ovolgelb  19368  dyadmax  19482  subopnmbl  19488  ismbf3d  19538  mbfimaopnlem  19539  mbfimaopn2  19541  mbfaddlem  19544  mbfsup  19548  mbfinf  19549  i1f1lem  19573  i1fmulclem  19586  itg1climres  19598  mbfi1fseqlem4  19602  itg2monolem1  19634  itg2gt0  19644  isibl  19649  iblcnlem1  19671  ellimc2  19756  dvcnvrelem1  19893  itgsubst  19925  mdegleb  19979  fta1glem2  20081  quotval  20201  vieta1lem1  20219  vieta1lem2  20220  ulm2  20293  ulmcaulem  20302  ulmcau  20303  radcnvlt1  20326  sineq0  20421  cos11  20427  recosf1o  20429  efopn  20541  cxpeq  20633  mcubic  20679  birthdaylem3  20784  rlimcnp  20796  xrlimcnp  20799  wilth  20846  isppw  20889  isppw2  20890  mumullem2  20955  sqff1o  20957  dvdsmulf1o  20971  fsumvma  20989  fsumvma2  20990  vmasum  20992  chpchtsum  20995  lgsne0  21109  lgseisenlem2  21126  lgsquadlem1  21130  lgsquadlem2  21131  dchrmusumlema  21179  rpvmasum2  21198  dchrisum0lema  21200  pntibndlem3  21278  pntlemi  21290  pntleml  21297  pnt3  21298  nbgraf1olem1  21443  nbgraf1olem5  21447  nbcusgra  21464  uvtx01vtx  21493  cusgrauvtxb  21497  iswlk  21519  istrl  21529  ispth  21560  isspth  21561  wlkdvspthlem  21599  usgrcyclnl2  21620  eupath2  21694  grpodiveq  21836  opidon  21902  issmgrp  21914  ismndo  21923  isrngo  21958  isdivrngo  22011  isvclem  22048  isnvlem  22081  isphg  22310  isph  22315  phoeqi  22351  ubthlem3  22366  minvecolem5  22375  minvecolem6  22376  minvecolem7  22377  hhph  22672  issh3  22714  nmopub  23403  nmfnleub  23420  adjeq  23430  adjvalval  23432  elunop2  23508  lnophm  23514  nmcexi  23521  cnlnadjlem5  23566  cnlnadjeui  23572  adjbd1o  23580  jpi  23765  mddmd2  23804  chrelati  23859  chrelat2i  23860  cvexchlem  23863  dmdbr5ati  23917  cdjreui  23927  cdj3i  23936  preqsnd  23992  abfmpunirn  24056  feqmptdf  24067  fmptcof2  24068  ofpreima  24073  funcnvmptOLD  24074  funcnvmpt  24075  funcnv5mpt  24076  iocinioc2  24134  eliccioo  24169  pstmxmet  24284  xrmulc1cn  24308  isrrvv  24693  eldmgm  24798  dmgmaddn0  24799  lgamgulmlem6  24810  subfacp1lem3  24860  subfacp1lem6  24863  subfacp1  24864  txpcon  24911  sconpi1  24918  rescon  24925  cvmscbv  24937  cvmsval  24945  cvmlift2lem13  24994  cvmlift3lem2  24999  cvmlift3  25007  divelunit  25177  br8  25371  br6  25372  br4  25373  distel  25423  elpred  25444  poseq  25520  wsuclem  25568  sltsolem1  25615  imageval  25767  funpartfv  25782  dfrdg4  25787  altopthg  25804  altopthbg  25805  brbtwn  25830  brcgr  25831  brbtwn2  25836  colinearalg  25841  axeuclidlem  25893  axcontlem2  25896  axcontlem4  25898  axcontlem7  25901  brcolinear2  25984  lineext  26002  brsegle  26034  seglelin  26042  broutsideof2  26048  onsuct0  26183  supaddc  26228  supadd  26229  mbfposadd  26244  cnambfre  26245  itg2addnclem2  26247  isfne4  26340  isfne2  26342  isfne3  26343  fneval  26358  topfneec  26362  neibastop2lem  26380  neibastop2  26381  neifg  26391  filnetlem4  26401  fdc  26440  heibor1  26510  rrncmslem  26532  rrnheibor  26537  isfldidl2  26670  isdmn3  26675  prtlem13  26708  prter3  26722  fnnfpeq0  26730  ralxpxfr2d  26732  ellz1  26816  lzunuz  26817  fz1eqin  26818  diophrex  26825  rexrabdioph  26845  rexfrabdioph  26846  2rexfrabdioph  26847  3rexfrabdioph  26848  4rexfrabdioph  26849  6rexfrabdioph  26850  7rexfrabdioph  26851  fzneg  27038  expdioph  27085  wepwsolem  27107  fnwe2lem2  27117  islmodfg  27135  kercvrlsm  27149  dsmmelbas  27173  ellspd  27222  islindf  27250  islindf4  27276  f1omvdconj  27357  sdrgacs  27477  pm10.52  27528  iotasbc  27587  pm14.122a  27590  pm14.122b  27591  pm14.123a  27593  rusbcALT  27607  fvsb  27622  stoweidlem34  27750  2reu4a  27934  sbcfun  27954  funressnfv  27959  dfafn5a  27991  el2xptp0  28051  otthg  28054  f12dfv  28066  f13dfv  28067  elfz2z  28089  euhash1  28145  usgra2pthlem1  28263  usg2spthonot  28308  frgra3vlem2  28328  frgrancvvdeqlem2  28357  frgrancvvdeqlem3  28358  frgrancvvdeqlemC  28365  usg2spot2nb  28391  gte-lte  28404  gt-lt  28405  bnj976  29085  bnj944  29246  bnj1173  29308  bnj1321  29333  bnj1373  29336  bnj1417  29347  ax12olem6NEW7  29396  sbcomwAUX7  29525  ax7w15lemAUX7  29604  ax7w15AUX7  29605  ax7w14AUX7  29607  sbcomOLD7  29692  lrelat  29749  islshpat  29752  lshpsmreu  29844  lkrpssN  29898  cmtvalN  29946  omllaw2N  29979  cvrval  30004  cvrval2  30009  cvlsupr3  30079  3dim0  30191  islln2  30245  islpln5  30269  islpln2  30270  islpln2ah  30283  islvol5  30313  islvol2  30314  4atlem11  30343  pmapglbx  30503  cdleme18d  31029  cdlemefrs29bpre0  31130  cdlemb3  31340  cdlemg33b  31441  dvhb1dimN  31720  dia11N  31783  cdlemm10N  31853  dib11N  31895  dib1dim  31900  dibglbN  31901  diblsmopel  31906  dihopelvalcpre  31983  dih11  32000  dihmeetlem4preN  32041  dihmeetlem13N  32054  lcfrvalsnN  32276  lcfrlem9  32285  lcf1o  32286  mapdval4N  32367  baerlem3lem2  32445  baerlem5alem2  32446  baerlem5blem2  32447  hdmap1fval  32532  hdmapfval  32565  hdmapglem7a  32665  hlhillcs  32696
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