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

Theorem syl5bb 267
Description: A syllogism inference from two biconditionals. (Contributed by NM, 12-Mar-1993.)
Hypotheses
Ref Expression
syl5bb.1 (𝜑𝜓)
syl5bb.2 (𝜒 → (𝜓𝜃))
Assertion
Ref Expression
syl5bb (𝜒 → (𝜑𝜃))

Proof of Theorem syl5bb
StepHypRef Expression
1 syl5bb.1 . . 3 (𝜑𝜓)
21a1i 11 . 2 (𝜒 → (𝜑𝜓))
3 syl5bb.2 . 2 (𝜒 → (𝜓𝜃))
42, 3bitrd 263 1 (𝜒 → (𝜑𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 191
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 192
This theorem is referenced by:  syl5rbb  268  syl5bbr  269  3bitr4g  298  imim21b  376  ifpfal  1008  cad0  1544  ax12wdemo  1959  sbal2  2344  necon3abid  2713  necon3bid  2721  ceqsralt  3092  ralxpxfr2d  3187  ceqsrexv  3195  ceqsrex2v  3197  elab2g  3211  elrabf  3218  elrab3t  3219  eueq2  3236  eqreu  3254  reu8  3258  ru  3290  sbcralt  3364  sbcabel  3369  sbcel1g  3816  sbcel2  3818  csbnestgf  3825  sbccsb2  3834  disjpss  3855  sbcssg  3907  rexsng  4035  ralprg  4049  rexprg  4050  difsn  4135  preq2b  4176  opthpr  4182  preqsnd  4188  ralunsn  4216  csbuni  4256  dfiin2g  4340  iunxsng  4389  elpwuni  4400  disjxun  4432  sbcbr12g  4488  pwnss  4606  opthneg  4722  otthg  4726  opelopabt  4754  opelopabga  4755  brabga  4756  csbmpt12  4776  rbropapd  4781  dfid3  4796  frirr  4857  wereu2  4877  brab2a  4931  opeliunxp  4933  posn  4950  sosn  4951  frsn  4952  brab2ga  4957  opbrop  4961  csbcnvgALT  5067  elrnmpt1  5132  elrnmptg  5133  eliniseg2  5259  poleloe  5281  xpdifid  5315  cnvpo  5425  elpred  5444  ordtri4  5511  oneqmini  5525  elsucg  5541  elsuc2g  5542  sbcfung  5656  dffun8  5660  fncnv  5702  fununi  5704  fnssresb  5743  fnimaeq0  5752  funcocnv2  5898  csbfv12  5965  dffn5  5975  funimass4  5981  feqmptdf  5985  fnsnfv  5992  dmfco  6006  fndmdif  6053  fvimacnvi  6063  fvimacnvALT  6068  unpreima  6073  respreima  6076  fmptco  6124  fressnfv  6146  fmptsnd  6154  fnnfpeq0  6163  tpres  6185  elunirn  6227  dff13  6230  f12dfv  6243  f13dfv  6244  fliftel  6273  isoini  6302  f1oiso  6315  eloprabga  6458  resoprab2  6468  elrnmpt2res  6485  ralrnmpt2  6486  ovid  6488  ov  6491  ovg  6510  ofrfval2  6625  dfwe2  6685  ssonprc  6696  ordpwsuc  6719  dfom2  6771  f1oweALT  6854  el2xptp0  6914  fmpt2x  6936  ovmptss  6956  1stconst  6963  2ndconst  6964  fnsuppres  7020  brtpos2  7056  mpt2curryd  7093  dfsmo2  7143  rdglim2  7227  seqomlem2  7245  omeu  7363  oeeui  7380  brdifun  7469  eqerlem  7474  brecop  7538  erovlem  7541  eceqoveq  7551  mapsn  7596  ixpsnval  7608  mptelixpg  7642  map1  7732  xpsnen  7740  xpdom2  7751  omxpenlem  7757  xpf1o  7818  mapunen  7825  onfin  7847  fimaxg  7903  fodomfib  7936  fofinf1o  7937  fipreima  7965  supub  8058  infglb  8089  infglbb  8090  fiming  8097  fiinfg  8098  ordtypecbv  8115  ordtypelem3  8118  ordtypelem9  8124  hartogslem1  8140  wofib  8143  wemapsolem  8148  wemapso2lem  8150  noinfep  8250  cantnf  8283  rankbnd2  8425  domtri2  8508  infxpenc2  8538  fseqdom  8542  acni2  8562  dfac9  8651  cfeq0  8771  cfsuc  8772  cflim3  8777  cfslb  8781  cofsmo  8784  enfin2i  8836  isfin3ds  8844  isf33lem  8881  fin1a2lem5  8919  axdc2lem  8963  zorn2g  9018  fodomb  9039  brdom7disj  9044  brdom6disj  9045  iundom2g  9050  cfpwsdom  9094  elgch  9132  fpwwe2cbv  9140  fpwwecbv  9154  pwfseqlem3  9170  pwfseqlem4a  9171  pwfseqlem4  9172  ltpiord  9397  nlt1pi  9416  nqereu  9439  addclprlem1  9526  1idpr  9539  reclem3pr  9559  ltsosr  9603  map2psrpr  9619  supsrlem  9620  axrrecex  9672  xrlenlt  9784  eqlei2  9830  addsubeq4  9977  renegcli  10022  lesub0  10219  wloglei  10234  conjmul  10413  rereccl  10414  infm3  10657  supaddc  10663  supadd  10664  supmul1  10665  supmullem1  10666  supmullem2  10667  supmul  10668  creui  10693  nndiv  10739  elznn0  11043  prime  11106  eqreznegel  11340  zsupss  11344  rebtwnz  11354  negelrp  11424  ltxr  11506  elixx3g  11743  ixxun  11746  ioo0  11756  ico0  11777  ioc0  11778  icc0  11779  difreicc  11860  divelunit  11870  iccf1o  11872  elfz2  11887  fzn  11911  fznn  11961  fzshftral  11980  nelfzo  12026  fzosplitsni  12125  om2uzisoi  12281  rabssnn0fi  12312  mptnn0fsupp  12323  sq11i  12479  hashsdom  12678  fi1uzind  12773  fi1uzindOLD  12779  wrdval  12802  csbwrdg  12828  wrd2ind  12967  s2f1o  13149  cjreb  13346  rexfiuz  13570  cau3lem  13577  rlim2  13720  ello12  13740  ello1mpt  13745  elo12  13751  o1lo1  13761  lo1resb  13788  o1resb  13790  o1compt  13811  caucvgb  13906  mertens  14102  ruclem12  14453  divides  14467  odd2np1  14526  oddm1even  14527  sadadd2lem2  14586  gcdcllem2  14636  bezoutlem2OLD  14666  bezoutlem3OLD  14667  bezoutlem4OLD  14668  bezoutlem2  14669  bezoutlem3  14670  bezoutlem4  14671  isprm2  14794  isprm3  14795  prmreclem2  15023  prmreclem5  15026  prmreclem6  15027  4sqlem2  15055  4sqlem12  15062  vdwmc  15090  vdwpc  15092  vdwlem6  15098  vdwlem10  15102  vdwnn  15110  ramval  15122  ramvalOLD  15123  0ram  15140  prdsleval  15540  pwsle  15555  imasleval  15612  xpsfrnel2  15636  xpsle  15652  isacs2  15725  mreacs  15730  acsfn  15731  iscatd2  15753  catpropd  15780  ciclcl  15873  cicrcl  15874  isssc  15891  evlfcl  16273  uncfcurf  16290  pltval  16371  lublecllem  16399  tosso  16447  oduleg  16543  oduclatb  16555  posglbmo  16558  isipodrs  16572  odudlatb  16607  gsumvalx  16678  sgrp2rid2  16820  grplmulf1o  16888  grplactcnv  16914  elnmz  17016  eqgid  17029  isghm  17043  ghmeqker  17069  resscntz  17146  symg1bas  17198  pgrpsubgsymgbi  17209  symgfixelq  17235  f1omvdconj  17248  odmulgeq  17369  sylow3lem3  17442  sylow3lem6  17445  efgval2  17535  efgsdm  17541  efgrelexlema  17560  efgcpbllemb  17566  iscyggen2  17677  cyggenod  17680  gsummptfzcl  17762  eldprd  17797  dprdf11  17816  dprddisj2  17832  pgpfac1lem2  17868  pgpfac1  17873  srg1zr  17922  drngid2  18151  issubrg  18168  islmod  18255  aspval2  18730  psrbag  18747  cply1coe0bi  19052  zndvds  19278  znleval  19283  iunocv  19402  pjfval2  19430  pjdm2  19432  dsmmelbas  19460  ellspd  19518  islindf  19528  islindf4  19554  istopg  20083  basgen2  20162  isclo  20260  mretopd  20265  isnei  20276  isperf3  20326  restdis  20351  neitr  20353  restcls  20354  restlp  20356  restperf  20357  iscn  20408  iscnp  20410  lmbr2  20432  lmbrf  20433  ordtt1  20552  cmpsub  20572  hauscmplem  20578  cmpfi  20580  dfcon2  20591  1stcelcls  20633  1stccn  20635  nllyi  20647  subislly  20653  dissnlocfin  20701  elkgen  20708  ptpjpre1  20743  ptuni2  20748  ptclsg  20787  ptcnplem  20793  txcn  20798  hausdiag  20817  txhaus  20819  txkgen  20824  xkoptsub  20826  cnmpt21  20843  elqtop  20869  tgqtop  20884  r0cld  20910  elfg  21044  fbasrn  21057  trfil2  21060  trfil3  21061  fin1aufil  21105  elfm2  21121  elfm3  21123  flimopn  21148  fbflim  21149  flfnei  21164  flftg  21169  cnpflf2  21173  txflf  21179  fclsbas  21194  alexsubALTlem4  21223  cnextfvval  21238  snclseqg  21288  tgphaus  21289  tsmsfbas  21300  tsmssubm  21315  utopsnneip  21421  prdsxmetlem  21541  imasdsf1olem  21546  xpsdsval  21554  blres  21604  isxms2  21621  metcnp  21714  txmetcnp  21720  txmetcn  21721  metustel  21723  metuel2  21738  dscopn  21746  isngp4  21783  cnblcld  21953  metnrmlem1a  22033  metnrmlem1aOLD  22048  icoopnst  22125  iocopnst  22126  elpi1  22235  lmmbr2  22388  cfil3i  22398  caucfil  22412  iscmet3  22422  lmclim  22431  metcld2  22435  bcthlem4  22454  minveclem3b  22529  minveclem6  22535  minveclem7  22536  minveclem3bOLD  22541  minveclem6OLD  22547  minveclem7OLD  22548  ivthle  22566  ivthle2  22567  evthicc2  22570  ovolfioo  22579  ovolficc  22580  ovolgelb  22592  dyadmax  22716  subopnmbl  22722  ismbf3d  22771  mbfimaopnlem  22772  mbfimaopn2  22774  mbfaddlem  22777  mbfsup  22781  mbfinf  22782  mbfinfOLD  22783  i1f1lem  22808  i1fmulclem  22821  itg1climres  22833  mbfi1fseqlem4  22837  itg2monolem1  22869  itg2gt0  22879  isibl  22884  iblcnlem1  22906  ellimc2  22993  dvcnvrelem1  23130  itgsubst  23162  mdegleb  23174  fta1glem2  23278  quotval  23406  vieta1lem1  23424  vieta1lem2  23425  ulm2  23501  ulmcaulem  23510  ulmcau  23511  radcnvlt1  23534  sineq0  23637  cos11  23643  recosf1o  23645  efopn  23764  cxpeq  23858  mcubic  23934  birthdaylem3  24040  rlimcnp  24052  xrlimcnp  24055  eldmgm  24108  dmgmaddn0  24109  lgamgulmlem6  24120  wilth  24157  isppw  24202  isppw2  24203  mumullem2  24268  sqff1o  24270  dvdsmulf1o  24284  fsumvma  24302  fsumvma2  24303  vmasum  24305  chpchtsum  24308  lgsne0  24422  lgseisenlem2  24439  lgsquadlem1  24443  lgsquadlem2  24444  dchrmusumlema  24492  rpvmasum2  24511  dchrisum0lema  24513  pntibndlem3  24591  pntlemi  24603  pntleml  24610  pnt3  24611  trgcgrg  24721  tgcgr4  24737  colcom  24764  colrot1  24765  ltgov  24803  hlcomb  24809  lncom  24828  mirreu3  24860  isperp  24918  perpcom  24919  brbtwn  25090  brcgr  25091  brbtwn2  25096  colinearalg  25101  axeuclidlem  25153  axcontlem2  25156  axcontlem4  25158  axcontlem7  25161  nbgraf1olem1  25330  nbgraf1olem5  25334  nbcusgra  25352  uvtx01vtx  25381  cusgrauvtxb  25385  iswlk  25409  istrl  25428  ispth  25459  isspth  25460  wlkdvspthlem  25498  usgrcyclnl2  25530  wwlkn0s  25594  wwlkextwrd  25617  wwlkextproplem3  25632  isclwlk0  25643  clwwlkn2  25664  eclclwwlkn1  25720  eleclclwwlkn  25721  hashecclwwlkn1  25722  usghashecclwwlk  25723  clwlkfclwwlk1hashn  25729  clwlkfoclwwlk  25733  usg2spthonot  25776  isrgra  25814  isrusgra  25815  isrusgusrg  25820  eupath2  25868  frgra3vlem2  25889  frgrancvvdeqlem2  25919  frgrancvvdeqlem3  25920  frgrancvvdeqlemC  25927  usg2spot2nb  25953  grpodiveq  26147  opidonOLD  26213  issmgrpOLD  26225  ismndo  26234  isrngo  26269  isdivrngo  26322  isvclem  26359  isnvlem  26392  isphg  26621  isph  26626  phoeqi  26662  ubthlem3  26677  minvecolem5  26686  minvecolem6  26687  minvecolem7  26688  minvecolem5OLD  26696  minvecolem6OLD  26697  minvecolem7OLD  26698  hhph  26994  issh3  27035  nmopub  27724  nmfnleub  27741  adjeq  27751  adjvalval  27753  elunop2  27829  lnophm  27835  nmcexi  27842  cnlnadjlem5  27887  cnlnadjeui  27893  adjbd1o  27901  jpi  28086  mddmd2  28125  chrelati  28180  chrelat2i  28181  cvexchlem  28184  dmdbr5ati  28238  cdjreui  28248  cdj3i  28257  iunxsngf  28332  disjunsn  28363  opeldifid  28368  fcoinvbr  28373  brabgaf  28374  opabdm  28377  opabrn  28378  iunsnima  28382  abfmpunirn  28409  fmptcof2  28416  funcnvmptOLD  28427  funcnvmpt  28428  funcnv5mpt  28429  f1od2  28465  resf1o  28471  fpwrelmap  28474  iocinioc2  28517  eliccioo  28556  posrasymb  28574  isslmd  28673  smatrcl  28777  pstmxmet  28855  prsdm  28875  prsrn  28876  ordtconlem1  28885  xrmulc1cn  28891  ispisys2  29130  elcarsg  29291  eulerpartlemmf  29362  isrrvv  29430  bnj976  29741  bnj944  29901  bnj1173  29963  bnj1321  29988  bnj1373  29991  bnj1417  30002  subfacp1lem3  30057  subfacp1lem6  30060  subfacp1  30061  txpcon  30107  sconpi1  30114  rescon  30121  cvmscbv  30133  cvmsval  30141  cvmlift2lem13  30190  cvmlift3lem2  30195  cvmlift3  30203  mclsrcl  30351  br8  30547  br6  30548  br4  30549  fv1stcnv  30573  fv2ndcnv  30574  distel  30601  poseq  30642  wsuclem  30659  sltsolem1  30708  imageval  30848  funpartfv  30863  dfrdg4  30869  altopthg  30885  altopthbg  30886  brcolinear2  30976  lineext  30994  brsegle  31026  seglelin  31034  broutsideof2  31040  isfne4  31145  isfne2  31147  isfne3  31148  fneval  31157  topfneec  31160  neibastop2lem  31165  neibastop2  31166  neifg  31176  filnetlem4  31186  onsuct0  31250  bj-abbi  31572  bj-tagcg  31765  bj-projval  31776  bj-restuni  31830  csbopg2  31946  csbwrecsg  31949  csboprabg  31952  csbmpt22g  31953  topdifinffinlem  31971  isbasisrelowllem1  31979  isbasisrelowllem2  31980  rdgeqoa  31994  csbfinxpg  32001  wl-sbrimt  32109  wl-sblimt  32110  wl-sbnf1  32114  wl-mo2df  32130  wl-eudf  32132  wl-mo2t  32135  wl-mo3t  32136  wl-ax11-lem6  32145  uncov  32159  tan2h  32170  matunitlindf  32176  ptrest  32177  poimirlem2  32180  poimirlem16  32194  poimirlem19  32197  poimirlem23  32201  poimirlem24  32202  poimirlem25  32203  poimirlem26  32204  poimirlem27  32205  mbfposadd  32226  cnambfre  32227  itg2addnclem2  32232  fdc  32311  heibor1  32379  rrncmslem  32401  rrnheibor  32406  isfldidl2  32539  isdmn3  32544  prtlem13  32673  prter3  32687  lrelat  32820  islshpat  32823  lshpsmreu  32915  lkrpssN  32969  cmtvalN  33017  omllaw2N  33050  cvrval  33075  cvrval2  33080  cvlsupr3  33150  3dim0  33262  islln2  33316  islpln5  33340  islpln2  33341  islpln2ah  33354  islvol5  33384  islvol2  33385  4atlem11  33414  pmapglbx  33574  cdleme18d  34101  cdlemefrs29bpre0  34203  cdlemb3  34413  cdlemg33b  34514  cdlemkid3N  34740  cdlemkid4  34741  dvhb1dimN  34793  dia11N  34856  cdlemm10N  34926  dib11N  34968  dib1dim  34973  dibglbN  34974  diblsmopel  34979  dihopelvalcpre  35056  dih11  35073  dihmeetlem4preN  35114  dihmeetlem13N  35127  lcfrvalsnN  35349  lcfrlem9  35358  lcf1o  35359  mapdval4N  35440  baerlem3lem2  35518  baerlem5alem2  35519  baerlem5blem2  35520  hdmap1fval  35605  hdmapfval  35638  hdmapglem7a  35738  hlhillcs  35769  ellz1  35849  lzunuz  35850  fz1eqin  35851  diophrex  35858  rexrabdioph  35877  rexfrabdioph  35878  2rexfrabdioph  35879  3rexfrabdioph  35880  4rexfrabdioph  35881  6rexfrabdioph  35882  7rexfrabdioph  35883  fzneg  36072  expdioph  36118  wepwsolem  36140  fnwe2lem2  36149  islmodfg  36167  kercvrlsm  36181  sdrgacs  36307  cnvcnvintabd  36445  iunrelexpuztr  36550  brtrclfv2  36558  frege124d  36592  rcompleq  36859  ntrclsneine0lem  36882  ntrclsiso  36885  ntrclsk2  36886  ntrclskb  36887  ntrneiiso  36902  ntrneikb  36905  k0004lem3  36945  pm10.52  37071  iotasbc  37127  pm14.122a  37130  pm14.122b  37131  pm14.123a  37133  rusbcALT  37147  fvsb  37162  trsbc  37257  rexsngf  37734  iunxsngf2  37744  mapsnd  37836  limcperiod  38112  limsupre  38125  limsupreOLD  38126  dvbdfbdioo  38221  stoweidlem34  38331  fourierdlem108  38514  fourierdlem110  38516  etransc  38585  2reu4a  39130  funressnfv  39149  dfafn5a  39182  el1fzopredsuc  39242  iccelpart  39267  dfeven2  39299  gboge7  39384  bgoldbwt  39398  riotaeqimp  39560  elfz2z  39577  isuhgr  39682  isushgr  39683  isupgr  39710  isumgr  39720  isuspgr  39782  isusgr  39783  uhgr0v0e  39864  isfusgrf1  39939  opfusgr  39942  usgr1v0e  39945  nbuhgr2vtx1edgb  39974  edgnbusgreu  39995  nbusgredgeu0  39996  isuvtxa  40021  cusgruvtxb  40044  cplgr3v  40057  cusgrsizeinds  40068  vtxdg0v  40088  vtxd0nedgb  40103  vtxduhgr0nedg  40107  vtxdusgr0edgnelALT  40111  is1wlk  40213  isWlk  40214  1wlk1walk  40243  upgr2wlk  40276  usgr2pthlem  40369  isclWlke  40384  isclWlkupgr  40385  iswwlksnx  40442  wwlksnextwrd  40503  wwlksnextproplem3  40517  umgr2wlk  40556  elwwlks2  40570  elwspths2spth  40571  clwlkclwwlk  40611  clwwlksn2  40617  eclclwwlksn1  40659  eleclclwwlksn  40660  hashecclwwlksn1  40661  umgrhashecclwwlk  40662  clwlksfclwwlk1hashn  40666  clwlksfoclwwlk  40670  clwwlksnun  40681  1pthon2v-av  40720  uhgr3cyclex  40749  isconngr  40756  isconngr1  40757  eupth2lems  40806  isfrgr  40830  frgr0v  40833  frgr3vlem2  40844  frgrncvvdeqlem2  40870  frgrncvvdeqlem3  40871  frgrncvvdeqlemC  40878  fusgr2wsp2nb  40898  ismhm0  40995  inclfusubc  41057  isrnghm  41082  rnghmval2  41085  uzlidlring  41119  lidldomnnring  41120  zrninitoringc  41263  opeliun2xp  41304  snlindsntor  41454  elbigo2  41552  gte-lte  41633  gt-lt  41634
  Copyright terms: Public domain W3C validator