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  2368  necon3abid  2454  necon3bid  2456  necon1abid  2474  r19.21t  2603  ceqsralt  2786  ceqsrexv  2876  ceqsrex2v  2878  elab2g  2891  elrabf  2897  eueq2  2914  eqreu  2932  reu8  2936  ru  2965  sbcralt  3038  sbcabel  3043  csbnestgf  3104  disjpss  3480  ralprg  3656  rexprg  3657  difsn  3729  opthpr  3764  ralunsn  3789  dfiin2g  3910  iunxsng  3954  elpwuni  3963  disjxun  3995  opelopabt  4249  opelopabga  4250  brabga  4251  dfid3  4282  frirr  4342  wereu2  4362  ordtri4  4401  oneqmini  4415  elsucg  4431  elsuc2g  4432  dfwe2  4545  ssonprc  4555  ordpwsuc  4578  dfom2  4630  brab2a  4726  opeliunxp  4728  posn  4746  sosn  4747  frsn  4748  brab2ga  4751  opbrop  4755  elrnmpt1  4916  elrnmptg  4917  eliniseg2  5041  poleloe  5065  cnvpo  5200  dffun8  5220  fncnv  5252  fununi  5254  fnssresb  5294  fnimaeq0  5303  funcocnv2  5436  dffn5  5502  funimass4  5507  fnsnfv  5516  dmfco  5527  fndmdif  5563  fvimacnvi  5573  fvimacnvALT  5578  unpreima  5585  respreima  5588  fmptco  5625  fressnfv  5641  fnsuppres  5666  elunirnALT  5713  dff13  5717  fliftel  5742  isoini  5769  f1oiso  5782  f1oweALT  5785  eloprabga  5868  resoprab2  5875  ralrnmpt2  5892  ovid  5898  ov  5901  ovg  5920  ofrfval2  6030  fmpt2x  6124  ovmptss  6134  1stconst  6141  2ndconst  6142  brtpos2  6174  pwnss  6265  dfsmo2  6332  tfrlem1  6359  rdglim2  6413  seqomlem2  6431  omeu  6551  oeeui  6568  brdifun  6655  eqerlem  6660  brecop  6719  erovlem  6722  eceqoveq  6731  mapsn  6777  mptelixpg  6821  map1  6907  xpsnen  6914  xpdom2  6925  omxpenlem  6931  xpf1o  6991  mapunen  6998  onfin  7019  fimaxg  7072  fodomfib  7104  fofinf1o  7105  fipreima  7129  supub  7178  ordtypecbv  7200  ordtypelem3  7203  ordtypelem9  7209  hartogslem1  7225  wofib  7228  wemapso2lem  7233  wemapso2  7235  noinfep  7328  noinfepOLD  7329  cantnf  7363  rankbnd2  7509  domtri2  7590  infxpenc2  7617  fseqdom  7621  acni2  7641  dfac9  7730  cfeq0  7850  cfsuc  7851  cflim3  7856  cfslb  7860  cofsmo  7863  enfin2i  7915  isfin3ds  7923  isf33lem  7960  fin1a2lem5  7998  axdc2lem  8042  zorn2g  8098  fodomb  8119  brdom7disj  8124  brdom6disj  8125  iundom2g  8130  cfpwsdom  8174  elgch  8212  fpwwe2cbv  8220  fpwwecbv  8234  pwfseqlem3  8250  pwfseqlem4a  8251  pwfseqlem4  8252  ltpiord  8479  nlt1pi  8498  nqereu  8521  addclprlem1  8608  1idpr  8621  reclem3pr  8641  ltsosr  8684  map2psrpr  8700  supsrlem  8701  axrrecex  8753  xrlenlt  8858  addsubeq4  9034  renegcli  9076  lesub0  9258  wloglei  9273  conjmul  9445  rereccl  9446  infm3  9681  supmul1  9687  supmullem1  9688  supmullem2  9689  supmul  9690  creui  9709  nndiv  9754  elznn0  10006  prime  10060  eqreznegel  10271  zsupss  10275  rebtwnz  10283  ltxr  10425  elixx3g  10636  ixxun  10639  ioo0  10648  ico0  10669  ioc0  10670  icc0  10671  difreicc  10734  iccf1o  10745  elfz2  10756  fzn  10777  fznn  10819  fzshftral  10836  fzosplitsni  10888  om2uzisoi  10984  sq11i  11161  hashsdom  11330  wrdval  11382  cjreb  11574  rexfiuz  11797  cau3lem  11804  rlim2  11936  ello12  11956  ello1mpt  11961  elo12  11967  o1lo1  11977  lo1resb  12004  o1resb  12006  o1compt  12027  caucvgb  12118  mertens  12305  ruclem12  12482  divides  12496  odd2np1  12550  oddm1even  12551  sadadd2lem2  12604  gcdcllem2  12654  bezoutlem2  12681  bezoutlem3  12682  bezoutlem4  12683  isprm2  12729  isprm3  12730  prmreclem2  12927  prmreclem5  12930  prmreclem6  12931  4sqlem2  12959  4sqlem12  12966  vdwmc  12988  vdwpc  12990  vdwlem6  12996  vdwlem10  13000  vdwnn  13008  ramval  13018  0ram  13030  prdsleval  13339  pwsle  13354  imasleval  13406  xpsfrnel2  13430  xpsle  13446  isacs2  13518  mreacs  13523  acsfn  13524  iscatd2  13546  catpropd  13575  isssc  13660  evlfcl  13959  uncfcurf  13976  pltval  14057  lubid  14079  tosso  14105  oduleg  14199  oduclatb  14211  isipodrs  14227  odudlatb  14262  spwpr2  14300  spwex  14301  gsumvalx  14414  grplmulf1o  14505  grplactcnv  14527  elnmz  14619  eqgid  14632  isghm  14646  ghmeqker  14672  resscntz  14770  odmulgeq  14833  sylow3lem3  14903  sylow3lem6  14906  efgval2  14996  efgsdm  15002  efgrelexlema  15021  efgcpbllemb  15027  iscyggen2  15131  cyggenod  15134  eldprd  15202  dprdf11  15221  dprddisj2  15237  pgpfac1lem2  15273  pgpfac1  15278  drngid2  15491  issubrg  15508  islmod  15594  aspval2  16049  psrbag  16075  zndvds  16466  znleval  16471  iunocv  16544  pjfval2  16572  pjdm2  16574  istopg  16604  istpsOLD  16621  basgen2  16690  isclo  16787  mretopd  16792  isnei  16803  isperf3  16847  restdis  16872  restcls  16874  restlp  16876  restperf  16877  iscn  16928  iscnp  16930  lmbr2  16952  lmbrf  16953  ordtt1  17070  cmpsub  17090  hauscmplem  17096  cmpfi  17098  dfcon2  17108  1stcelcls  17150  1stccn  17152  nllyi  17164  subislly  17170  elkgen  17194  ptpjpre1  17229  ptuni2  17234  ptclsg  17272  ptcnplem  17278  txcn  17283  hausdiag  17302  txhaus  17304  txkgen  17309  xkoptsub  17311  cnmpt21  17328  elqtop  17351  tgqtop  17366  r0cld  17392  elfg  17529  fbasrn  17542  trfil2  17545  trfil3  17546  fin1aufil  17590  elfm2  17606  elfm3  17608  flimopn  17633  fbflim  17634  flfnei  17649  flftg  17654  cnpflf2  17658  txflf  17664  fclsbas  17679  alexsubALTlem4  17707  snclseqg  17761  tgphaus  17762  tsmsfbas  17773  tsmssubm  17788  prdsxmetlem  17895  imasdsf1olem  17900  xpsdsval  17908  blres  17940  isxms2  17957  metcnp  18050  txmetcnp  18056  txmetcn  18057  dscopn  18059  isngp4  18096  cnblcld  18247  metnrmlem1a  18325  icoopnst  18400  iocopnst  18401  elpi1  18506  lmmbr2  18648  cfil3i  18658  caucfil  18672  iscmet3  18682  lmclim  18691  metcld2  18695  bcthlem4  18712  minveclem3b  18755  minveclem6  18761  minveclem7  18762  ivthle  18779  ivthle2  18780  evthicc2  18783  ovolfioo  18790  ovolficc  18791  ovolgelb  18802  dyadmax  18916  subopnmbl  18922  ismbf3d  18972  mbfimaopnlem  18973  mbfimaopn2  18975  mbfaddlem  18978  mbfsup  18982  mbfinf  18983  i1f1lem  19007  i1fmulclem  19020  itg1climres  19032  mbfi1fseqlem4  19036  itg2monolem1  19068  itg2gt0  19078  isibl  19083  iblcnlem1  19105  ellimc2  19190  dvcnvrelem1  19327  itgsubst  19359  mdegleb  19413  fta1glem2  19515  quotval  19635  vieta1lem1  19653  vieta1lem2  19654  ulm2  19727  ulmcaulem  19734  ulmcau  19735  radcnvlt1  19757  sineq0  19852  cos11  19858  recosf1o  19860  efopn  19968  cxpeq  20060  mcubic  20106  birthdaylem3  20211  rlimcnp  20223  xrlimcnp  20226  wilth  20272  isppw  20315  isppw2  20316  mumullem2  20381  sqff1o  20383  dvdsmulf1o  20397  fsumvma  20415  fsumvma2  20416  vmasum  20418  chpchtsum  20421  lgsne0  20535  lgseisenlem2  20552  lgsquadlem1  20556  lgsquadlem2  20557  dchrmusumlema  20605  rpvmasum2  20624  dchrisum0lema  20626  pntibndlem3  20704  pntlemi  20716  pntleml  20723  pnt3  20724  grpodiveq  20884  opidon  20950  issmgrp  20962  ismndo  20971  isrngo  21006  isdivrngo  21059  isvclem  21094  isnvlem  21127  isphg  21356  isph  21361  phoeqi  21397  ubthlem3  21412  minvecolem5  21421  minvecolem6  21422  minvecolem7  21423  hhph  21718  issh3  21760  nmopub  22449  nmfnleub  22466  adjeq  22476  adjvalval  22478  elunop2  22554  lnophm  22560  nmcexi  22567  cnlnadjlem5  22612  cnlnadjeui  22618  adjbd1o  22626  jpi  22811  mddmd2  22850  chrelati  22905  chrelat2i  22906  cvexchlem  22909  dmdbr5ati  22963  cdjreui  22973  cdj3i  22982  ballotlemfmpn  23015  eldmgm  23067  dmgmaddn0  23068  subfacp1lem3  23086  subfacp1lem6  23089  subfacp1  23090  txpcon  23136  sconpi1  23143  rescon  23150  cvmscbv  23162  cvmsval  23170  cvmlift2lem13  23219  cvmlift3lem2  23224  cvmlift3  23232  eupath2  23277  divelunit  23452  br8  23485  br6  23486  br4  23487  distel  23530  elpred  23547  poseq  23623  axsltsolem1  23691  axfelem20  23735  imageval  23845  dfrdg4  23864  altopthg  23877  altopthbg  23878  brbtwn  23903  brcgr  23904  brbtwn2  23909  colinearalg  23914  axeuclidlem  23966  axcontlem2  23969  axcontlem4  23971  axcontlem7  23974  brcolinear2  24057  lineext  24075  brsegle  24107  seglelin  24115  broutsideof2  24121  bpolyval  24160  onsuct0  24256  fnovpop  24405  twsymr  24445  prj1b  24446  prj3  24447  inttpemp  24507  repcpwti  24529  vecval1b  24819  svs2  24855  fgsb2  24923  islimrs3  24949  islimrs4  24950  bwt2  24960  supnuf  24997  supexr  24999  tcnvec  25058  ismgra  25078  isalg  25089  isded  25104  iscatOLD  25122  dualcat2  25152  issrc  25235  vtarsuelt  25263  sgplpte21a  25501  isibcg  25559  isfne4  25637  isfne2  25639  isfne3  25640  fneval  25655  topfneec  25659  neibastop2lem  25677  neibastop2  25678  neifg  25688  filnetlem4  25698  fdc  25823  heibor1  25902  rrncmslem  25924  rrnheibor  25929  isfldidl2  26062  isdmn3  26067  prtlem13  26104  prter3  26118  fnnfpeq0  26126  ralxpxfr2d  26128  ellz1  26214  lzunuz  26215  fz1eqin  26216  diophrex  26223  rexrabdioph  26243  rexfrabdioph  26244  2rexfrabdioph  26245  3rexfrabdioph  26246  4rexfrabdioph  26247  6rexfrabdioph  26248  7rexfrabdioph  26249  fzneg  26437  expdioph  26484  wepwsolem  26506  fnwe2lem2  26516  islmodfg  26535  kercvrlsm  26549  dsmmelbas  26573  ellspd  26622  islindf  26650  islindf4  26676  f1omvdconj  26757  sdrgacs  26877  pm10.52  26928  iotasbc  26988  pm14.122a  26991  pm14.122b  26992  pm14.123a  26994  rusbcALT  27008  fvsb  27024  stoweidlem34  27152  2reu4a  27316  gte-lte  27327  gt-lt  27328  bnj976  27941  bnj944  28102  bnj1173  28164  bnj1321  28189  bnj1373  28192  bnj1417  28203  ax11wdemoK  28275  ax12olem27X  28332  lrelat  28454  islshpat  28457  lshpsmreu  28549  lkrpssN  28603  cmtvalN  28651  omllaw2N  28684  cvrval  28709  cvrval2  28714  cvlsupr3  28784  3dim0  28896  islln2  28950  islpln5  28974  islpln2  28975  islpln2ah  28988  islvol5  29018  islvol2  29019  4atlem11  29048  pmapglbx  29208  cdleme18d  29734  cdlemefrs29bpre0  29835  cdlemb3  30045  cdlemg33b  30146  dvhb1dimN  30425  dia11N  30488  cdlemm10N  30558  dib11N  30600  dib1dim  30605  dibglbN  30606  diblsmopel  30611  dihopelvalcpre  30688  dih11  30705  dihmeetlem4preN  30746  dihmeetlem13N  30759  lcfrvalsnN  30981  lcfrlem9  30990  lcf1o  30991  mapdval4N  31072  baerlem3lem2  31150  baerlem5alem2  31151  baerlem5blem2  31152  hdmap1fval  31237  hdmapfval  31270  hdmapglem7a  31370  hlhillcs  31401
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