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

Theorem syl5bb 250
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 12 . 2  |-  ( ch 
->  ( ph  <->  ps )
)
3 syl5bb.2 . 2  |-  ( ch 
->  ( ps  <->  th )
)
42, 3bitrd 246 1  |-  ( ch 
->  ( ph  <->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178
This theorem is referenced by:  syl5rbb  251  syl5bbr  252  3bitr4g  281  imim21b  358  cad0  1396  had1  1398  ax12olem27  1661  sbcom  1984  abbi  2366  necon3abid  2452  necon3bid  2454  necon1abid  2472  r19.21t  2601  ceqsralt  2779  ceqsrexv  2869  ceqsrex2v  2871  elab2g  2884  elrabf  2890  eueq2  2907  eqreu  2925  reu8  2929  ru  2951  sbcralt  3024  sbcabel  3029  csbnestgf  3090  disjpss  3466  ralprg  3642  rexprg  3643  difsn  3715  opthpr  3750  ralunsn  3775  dfiin2g  3896  iunxsng  3940  elpwuni  3949  disjxun  3981  opelopabt  4235  opelopabga  4236  brabga  4237  dfid3  4268  frirr  4328  wereu2  4348  ordtri4  4387  oneqmini  4401  elsucg  4417  elsuc2g  4418  dfwe2  4531  ssonprc  4541  ordpwsuc  4564  dfom2  4616  brab2a  4712  opeliunxp  4714  posn  4732  sosn  4733  frsn  4734  brab2ga  4737  opbrop  4741  elrnmpt1  4902  elrnmptg  4903  eliniseg2  5027  poleloe  5051  cnvpo  5186  dffun8  5206  fncnv  5238  fununi  5240  fnssresb  5280  fnimaeq0  5289  funcocnv2  5422  dffn5  5488  funimass4  5493  fnsnfv  5502  dmfco  5513  fndmdif  5549  fvimacnvi  5559  fvimacnvALT  5564  unpreima  5571  respreima  5574  fmptco  5611  fressnfv  5627  fnsuppres  5652  elunirnALT  5699  dff13  5703  fliftel  5728  isoini  5755  f1oiso  5768  f1oweALT  5771  eloprabga  5854  resoprab2  5861  ralrnmpt2  5878  ovid  5884  ov  5887  ovg  5906  ofrfval2  6016  fmpt2x  6110  ovmptss  6120  1stconst  6127  2ndconst  6128  brtpos2  6160  pwnss  6251  dfsmo2  6318  tfrlem1  6345  rdglim2  6399  seqomlem2  6417  omeu  6537  oeeui  6554  brdifun  6641  eqerlem  6646  brecop  6705  erovlem  6708  eceqoveq  6717  mapsn  6763  mptelixpg  6807  map1  6893  xpsnen  6900  xpdom2  6911  omxpenlem  6917  xpf1o  6977  mapunen  6984  onfin  7005  fimaxg  7058  fodomfib  7090  fofinf1o  7091  fipreima  7115  supub  7164  ordtypecbv  7186  ordtypelem3  7189  ordtypelem9  7195  hartogslem1  7211  wofib  7214  wemapso2lem  7219  wemapso2  7221  noinfep  7314  noinfepOLD  7315  cantnf  7349  rankbnd2  7495  domtri2  7576  infxpenc2  7603  fseqdom  7607  acni2  7627  dfac9  7716  cfeq0  7836  cfsuc  7837  cflim3  7842  cfslb  7846  cofsmo  7849  enfin2i  7901  isfin3ds  7909  isf33lem  7946  fin1a2lem5  7984  axdc2lem  8028  zorn2g  8084  fodomb  8105  brdom7disj  8110  brdom6disj  8111  iundom2g  8116  cfpwsdom  8160  elgch  8198  fpwwe2cbv  8206  fpwwecbv  8220  pwfseqlem3  8236  pwfseqlem4a  8237  pwfseqlem4  8238  ltpiord  8465  nlt1pi  8484  nqereu  8507  addclprlem1  8594  1idpr  8607  reclem3pr  8627  ltsosr  8670  map2psrpr  8686  supsrlem  8687  axrrecex  8739  xrlenlt  8844  addsubeq4  9020  renegcli  9062  lesub0  9244  wloglei  9259  conjmul  9431  rereccl  9432  infm3  9667  supmul1  9673  supmullem1  9674  supmullem2  9675  supmul  9676  creui  9695  nndiv  9740  elznn0  9991  prime  10045  eqreznegel  10256  zsupss  10260  rebtwnz  10268  ltxr  10410  elixx3g  10621  ixxun  10624  ioo0  10633  ico0  10654  ioc0  10655  icc0  10656  difreicc  10719  iccf1o  10730  elfz2  10741  fzn  10762  fznn  10804  fzshftral  10821  fzosplitsni  10873  om2uzisoi  10969  sq11i  11146  hashsdom  11315  wrdval  11367  cjreb  11559  rexfiuz  11782  cau3lem  11789  rlim2  11921  ello12  11941  ello1mpt  11946  elo12  11952  o1lo1  11962  lo1resb  11989  o1resb  11991  o1compt  12012  caucvgb  12103  mertens  12290  ruclem12  12467  divides  12481  odd2np1  12535  oddm1even  12536  sadadd2lem2  12589  gcdcllem2  12639  bezoutlem2  12666  bezoutlem3  12667  bezoutlem4  12668  isprm2  12714  isprm3  12715  prmreclem2  12912  prmreclem5  12915  prmreclem6  12916  4sqlem2  12944  4sqlem12  12951  vdwmc  12973  vdwpc  12975  vdwlem6  12981  vdwlem10  12985  vdwnn  12993  ramval  13003  0ram  13015  prdsleval  13324  pwsle  13339  imasleval  13391  xpsfrnel2  13415  xpsle  13431  isacs2  13503  mreacs  13508  acsfn  13509  iscatd2  13531  catpropd  13560  isssc  13645  evlfcl  13944  uncfcurf  13961  pltval  14042  lubid  14064  tosso  14090  oduleg  14184  oduclatb  14196  isipodrs  14212  odudlatb  14247  spwpr2  14285  spwex  14286  gsumvalx  14399  grplmulf1o  14490  grplactcnv  14512  elnmz  14604  eqgid  14617  isghm  14631  ghmeqker  14657  resscntz  14755  odmulgeq  14818  sylow3lem3  14888  sylow3lem6  14891  efgval2  14981  efgsdm  14987  efgrelexlema  15006  efgcpbllemb  15012  iscyggen2  15116  cyggenod  15119  eldprd  15187  dprdf11  15206  dprddisj2  15222  pgpfac1lem2  15258  pgpfac1  15263  drngid2  15476  issubrg  15493  islmod  15579  aspval2  16034  psrbag  16060  zndvds  16451  znleval  16456  iunocv  16529  pjfval2  16557  pjdm2  16559  istopg  16589  istpsOLD  16606  basgen2  16675  isclo  16772  mretopd  16777  isnei  16788  isperf3  16832  restdis  16857  restcls  16859  restlp  16861  restperf  16862  iscn  16913  iscnp  16915  lmbr2  16937  lmbrf  16938  ordtt1  17055  cmpsub  17075  hauscmplem  17081  cmpfi  17083  dfcon2  17093  1stcelcls  17135  1stccn  17137  nllyi  17149  subislly  17155  elkgen  17179  ptpjpre1  17214  ptuni2  17219  ptclsg  17257  ptcnplem  17263  txcn  17268  hausdiag  17287  txhaus  17289  txkgen  17294  xkoptsub  17296  cnmpt21  17313  elqtop  17336  tgqtop  17351  r0cld  17377  elfg  17514  fbasrn  17527  trfil2  17530  trfil3  17531  fin1aufil  17575  elfm2  17591  elfm3  17593  flimopn  17618  fbflim  17619  flfnei  17634  flftg  17639  cnpflf2  17643  txflf  17649  fclsbas  17664  alexsubALTlem4  17692  snclseqg  17746  tgphaus  17747  tsmsfbas  17758  tsmssubm  17773  prdsxmetlem  17880  imasdsf1olem  17885  xpsdsval  17893  blres  17925  isxms2  17942  metcnp  18035  txmetcnp  18041  txmetcn  18042  dscopn  18044  isngp4  18081  cnblcld  18232  metnrmlem1a  18310  icoopnst  18385  iocopnst  18386  elpi1  18491  lmmbr2  18633  cfil3i  18643  caucfil  18657  iscmet3  18667  lmclim  18676  metcld2  18680  bcthlem4  18697  minveclem3b  18740  minveclem6  18746  minveclem7  18747  ivthle  18764  ivthle2  18765  evthicc2  18768  ovolfioo  18775  ovolficc  18776  ovolgelb  18787  dyadmax  18901  subopnmbl  18907  ismbf3d  18957  mbfimaopnlem  18958  mbfimaopn2  18960  mbfaddlem  18963  mbfsup  18967  mbfinf  18968  i1f1lem  18992  i1fmulclem  19005  itg1climres  19017  mbfi1fseqlem4  19021  itg2monolem1  19053  itg2gt0  19063  isibl  19068  iblcnlem1  19090  ellimc2  19175  dvcnvrelem1  19312  itgsubst  19344  mdegleb  19398  fta1glem2  19500  quotval  19620  vieta1lem1  19638  vieta1lem2  19639  ulm2  19712  ulmcaulem  19719  ulmcau  19720  radcnvlt1  19742  sineq0  19837  cos11  19843  recosf1o  19845  efopn  19953  cxpeq  20045  mcubic  20091  birthdaylem3  20196  rlimcnp  20208  xrlimcnp  20211  wilth  20257  isppw  20300  isppw2  20301  mumullem2  20366  sqff1o  20368  dvdsmulf1o  20382  fsumvma  20400  fsumvma2  20401  vmasum  20403  chpchtsum  20406  lgsne0  20520  lgseisenlem2  20537  lgsquadlem1  20541  lgsquadlem2  20542  dchrmusumlema  20590  rpvmasum2  20609  dchrisum0lema  20611  pntibndlem3  20689  pntlemi  20701  pntleml  20708  pnt3  20709  grpodiveq  20869  opidon  20935  issmgrp  20947  ismndo  20956  isrngo  20991  isdivrngo  21044  isvclem  21079  isnvlem  21112  isphg  21341  isph  21346  phoeqi  21382  ubthlem3  21397  minvecolem5  21406  minvecolem6  21407  minvecolem7  21408  hhph  21703  issh3  21745  nmopub  22434  nmfnleub  22451  adjeq  22461  adjvalval  22463  elunop2  22539  lnophm  22545  nmcexi  22552  cnlnadjlem5  22597  cnlnadjeui  22603  adjbd1o  22611  jpi  22796  mddmd2  22835  chrelati  22890  chrelat2i  22891  cvexchlem  22894  dmdbr5ati  22948  cdjreui  22958  cdj3i  22967  ballotlemfmpn  23000  eldmgm  23052  dmgmaddn0  23053  subfacp1lem3  23071  subfacp1lem6  23074  subfacp1  23075  txpcon  23121  sconpi1  23128  rescon  23135  cvmscbv  23147  cvmsval  23155  cvmlift2lem13  23204  cvmlift3lem2  23209  cvmlift3  23217  eupath2  23262  divelunit  23437  br8  23470  br6  23471  br4  23472  distel  23515  elpred  23532  poseq  23608  axsltsolem1  23676  axfelem20  23720  imageval  23830  dfrdg4  23849  altopthg  23862  altopthbg  23863  brbtwn  23888  brcgr  23889  brbtwn2  23894  colinearalg  23899  axeuclidlem  23951  axcontlem2  23954  axcontlem4  23956  axcontlem7  23959  brcolinear2  24042  lineext  24060  brsegle  24092  seglelin  24100  broutsideof2  24106  bpolyval  24145  onsuct0  24241  fnovpop  24390  twsymr  24430  prj1b  24431  prj3  24432  inttpemp  24492  repcpwti  24514  vecval1b  24804  svs2  24840  fgsb2  24908  islimrs3  24934  islimrs4  24935  bwt2  24945  supnuf  24982  supexr  24984  tcnvec  25043  ismgra  25063  isalg  25074  isded  25089  iscatOLD  25107  dualcat2  25137  issrc  25220  vtarsuelt  25248  sgplpte21a  25486  isibcg  25544  isfne4  25622  isfne2  25624  isfne3  25625  fneval  25640  topfneec  25644  neibastop2lem  25662  neibastop2  25663  neifg  25673  filnetlem4  25683  fdc  25808  heibor1  25887  rrncmslem  25909  rrnheibor  25914  isfldidl2  26047  isdmn3  26052  prtlem13  26089  prter3  26103  fnnfpeq0  26111  ralxpxfr2d  26113  ellz1  26199  lzunuz  26200  fz1eqin  26201  diophrex  26208  rexrabdioph  26228  rexfrabdioph  26229  2rexfrabdioph  26230  3rexfrabdioph  26231  4rexfrabdioph  26232  6rexfrabdioph  26233  7rexfrabdioph  26234  fzneg  26422  expdioph  26469  wepwsolem  26491  fnwe2lem2  26501  islmodfg  26520  kercvrlsm  26534  dsmmelbas  26558  ellspd  26607  islindf  26635  islindf4  26661  f1omvdconj  26742  sdrgacs  26862  pm10.52  26913  iotasbc  26973  pm14.122a  26976  pm14.122b  26977  pm14.123a  26979  rusbcALT  26993  fvsb  27009  stoweidlem34  27104  gte-lte  27227  gt-lt  27228  bnj976  27842  bnj944  28003  bnj1173  28065  bnj1321  28090  bnj1373  28093  bnj1417  28104  ax11wdemoK  28176  ax12olem27X  28233  lrelat  28355  islshpat  28358  lshpsmreu  28450  lkrpssN  28504  cmtvalN  28552  omllaw2N  28585  cvrval  28610  cvrval2  28615  cvlsupr3  28685  3dim0  28797  islln2  28851  islpln5  28875  islpln2  28876  islpln2ah  28889  islvol5  28919  islvol2  28920  4atlem11  28949  pmapglbx  29109  cdleme18d  29635  cdlemefrs29bpre0  29736  cdlemb3  29946  cdlemg33b  30047  dvhb1dimN  30326  dia11N  30389  cdlemm10N  30459  dib11N  30501  dib1dim  30506  dibglbN  30507  diblsmopel  30512  dihopelvalcpre  30589  dih11  30606  dihmeetlem4preN  30647  dihmeetlem13N  30660  lcfrvalsnN  30882  lcfrlem9  30891  lcf1o  30892  mapdval4N  30973  baerlem3lem2  31051  baerlem5alem2  31052  baerlem5blem2  31053  hdmap1fval  31138  hdmapfval  31171  hdmapglem7a  31271  hlhillcs  31302
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator