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

Theorem syl5bb 270
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 266 1 (𝜒 → (𝜑𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194
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 195
This theorem is referenced by:  syl5rbb  271  syl5bbr  272  3bitr4g  301  imim21b  380  ifpfal  1017  cad0  1546  ax12wdemo  1960  sbal2  2353  necon3abid  2722  necon3bid  2730  ralxpxfr2d  3202  ceqsrexv  3210  ceqsrex2v  3212  elab2g  3226  elrabf  3233  elrab3t  3234  eueq2  3251  eqreu  3269  reu8  3273  ru  3305  sbcralt  3381  sbcabel  3387  sbcel1g  3842  sbcel2  3844  csbnestgf  3851  sbccsb2  3860  disjpss  3883  sbcssg  3938  rexsng  4069  ralprg  4084  rexprg  4085  difsn  4172  preq2b  4217  opthpr  4223  preqsnd  4229  csbopg  4256  ralunsn  4258  csbuni  4300  dfiin2g  4387  iunxsng  4436  elpwuni  4447  disjxun  4479  sbcbr12g  4536  pwnss  4655  opthneg  4774  otthg  4778  opelopabt  4806  opelopabga  4807  brabga  4808  opelopabgf  4814  csbmpt12  4828  rbropapd  4833  dfid3  4848  frirr  4909  wereu2  4929  brab2a  4985  opeliunxp  4987  posn  5004  sosn  5005  frsn  5006  brab2ga  5011  opbrop  5015  csbcnvgALT  5121  elrnmpt1  5186  elrnmptg  5187  eliniseg2  5315  poleloe  5337  xpdifid  5371  cnvpo  5480  elpred  5500  ordtri4  5568  oneqmini  5583  elsucg  5599  elsuc2g  5600  sbcfung  5717  dffun8  5721  fncnv  5766  fununi  5768  fnssresb  5807  fnimaeq0  5816  funcocnv2  5963  csbfv12  6030  dffn5  6040  funimass4  6046  feqmptdf  6050  fnsnfv  6057  dmfco  6071  fndmdif  6118  fvimacnvi  6128  fvimacnvALT  6133  unpreima  6138  respreima  6141  fmptco  6192  fressnfv  6214  fmptsnd  6222  fnnfpeq0  6231  tpres  6253  elunirn  6295  dff13  6298  f12dfv  6311  f13dfv  6312  fliftel  6341  isoini  6370  f1oiso  6383  eloprabga  6527  resoprab2  6537  elrnmpt2res  6554  ralrnmpt2  6555  ovid  6557  ov  6560  ovg  6579  ofrfval2  6694  dfwe2  6754  ssonprc  6765  ordpwsuc  6788  dfom2  6840  f1oweALT  6923  el2xptp0  6983  fmpt2x  7005  ovmptss  7025  1stconst  7032  2ndconst  7033  fnsuppres  7089  brtpos2  7125  mpt2curryd  7162  dfsmo2  7211  rdglim2  7295  seqomlem2  7313  omeu  7432  oeeui  7449  brdifun  7538  eqerlem  7543  brecop  7607  erovlem  7610  eceqoveq  7620  mapsn  7665  ixpsnval  7677  mptelixpg  7711  map1  7801  xpsnen  7809  xpdom2  7820  omxpenlem  7826  xpf1o  7887  mapunen  7894  onfin  7916  fimaxg  7972  fodomfib  8005  fofinf1o  8006  fipreima  8035  supub  8128  infglb  8159  infglbb  8160  fiming  8167  fiinfg  8168  ordtypecbv  8185  ordtypelem3  8188  ordtypelem9  8194  hartogslem1  8210  wofib  8213  wemapsolem  8218  wemapso2lem  8220  noinfep  8320  cantnf  8353  rankbnd2  8495  domtri2  8578  infxpenc2  8608  fseqdom  8612  acni2  8632  dfac9  8721  cfeq0  8841  cfsuc  8842  cflim3  8847  cfslb  8851  cofsmo  8854  enfin2i  8906  isfin3ds  8914  isf33lem  8951  fin1a2lem5  8989  axdc2lem  9033  zorn2g  9088  fodomb  9109  brdom7disj  9114  brdom6disj  9115  iundom2g  9121  cfpwsdom  9165  elgch  9203  fpwwe2cbv  9211  fpwwecbv  9225  pwfseqlem3  9241  pwfseqlem4a  9242  pwfseqlem4  9243  ltpiord  9468  nlt1pi  9487  nqereu  9510  addclprlem1  9597  1idpr  9610  reclem3pr  9630  ltsosr  9674  map2psrpr  9690  supsrlem  9691  axrrecex  9743  xrlenlt  9857  eqlei2  9903  addsubeq4  10051  renegcli  10097  lesub0  10298  wloglei  10313  conjmul  10495  rereccl  10496  infm3  10739  supaddc  10745  supadd  10746  supmul1  10747  supmullem1  10748  supmullem2  10749  supmul  10750  creui  10774  nndiv  10820  elznn0  11137  prime  11202  eqreznegel  11520  zsupss  11523  rebtwnz  11533  negelrp  11610  ltxr  11698  elixx3g  11932  ixxun  11935  ioo0  11944  ico0  11965  ioc0  11966  icc0  11967  difreicc  12048  divelunit  12058  iccf1o  12060  elfz2  12076  fzn  12100  fznn  12150  fzshftral  12169  nelfzo  12216  fzosplitsni  12316  om2uzisoi  12487  rabssnn0fi  12519  mptnn0fsupp  12531  sq11i  12688  hashsdom  12900  fi1uzind  12997  fi1uzindOLD  13003  wrdval  13026  csbwrdg  13052  wrd2ind  13192  s2f1o  13374  cjreb  13574  rexfiuz  13798  cau3lem  13805  rlim2  13945  ello12  13965  ello1mpt  13970  elo12  13976  o1lo1  13986  lo1resb  14013  o1resb  14015  o1compt  14036  caucvgb  14131  pwm1geoser  14312  mertens  14330  ruclem12  14682  divides  14696  dvdsabseq  14746  odd2np1  14776  oddm1even  14778  sumodd  14822  divalgmod  14843  modremain  14846  sadadd2lem2  14887  gcdcllem2  14937  bezoutlem2OLD  14972  bezoutlem3OLD  14973  bezoutlem4OLD  14974  bezoutlem2  14975  bezoutlem3  14976  bezoutlem4  14977  isprm2  15113  isprm3  15114  dvdsnprmd  15121  oddprmdvds  15333  prmreclem2  15347  prmreclem5  15350  prmreclem6  15351  4sqlem2  15379  4sqlem12  15386  vdwmc  15408  vdwpc  15410  vdwlem6  15416  vdwlem10  15420  vdwnn  15428  ramval  15438  0ram  15450  prdsleval  15848  pwsle  15863  imasleval  15920  xpsfrnel2  15944  xpsle  15960  isacs2  16033  mreacs  16038  acsfn  16039  iscatd2  16061  catpropd  16088  ciclcl  16181  cicrcl  16182  isssc  16199  evlfcl  16581  uncfcurf  16598  pltval  16679  lublecllem  16707  tosso  16755  oduleg  16851  oduclatb  16863  posglbmo  16866  isipodrs  16880  odudlatb  16915  gsumvalx  16989  sgrp2rid2  17132  grplmulf1o  17208  grplactcnv  17237  elnmz  17352  eqgid  17365  isghm  17379  ghmeqker  17406  resscntz  17483  symg1bas  17535  pgrpsubgsymgbi  17546  symgfixelq  17572  f1omvdconj  17585  odmulgeq  17706  sylow3lem3  17779  sylow3lem6  17782  efgval2  17872  efgsdm  17878  efgrelexlema  17897  efgcpbllemb  17903  iscyggen2  18017  cyggenod  18020  gsummptfzcl  18102  eldprd  18137  dprdf11  18156  dprddisj2  18172  pgpfac1lem2  18208  pgpfac1  18213  srg1zr  18263  drngid2  18497  issubrg  18514  islmod  18601  aspval2  19076  psrbag  19093  cply1coe0bi  19399  zndvds  19627  znleval  19632  iunocv  19751  pjfval2  19779  pjdm2  19781  dsmmelbas  19809  ellspd  19867  islindf  19877  islindf4  19903  istopg  20432  basgen2  20511  isclo  20608  mretopd  20613  isnei  20624  isperf3  20674  restdis  20699  neitr  20701  restcls  20702  restlp  20704  restperf  20705  iscn  20756  iscnp  20758  lmbr2  20780  lmbrf  20781  ordtt1  20900  cmpsub  20920  hauscmplem  20926  cmpfi  20928  dfcon2  20939  1stcelcls  20981  1stccn  20983  nllyi  20995  subislly  21001  dissnlocfin  21049  elkgen  21056  ptpjpre1  21091  ptuni2  21096  ptclsg  21135  ptcnplem  21141  txcn  21146  hausdiag  21165  txhaus  21167  txkgen  21172  xkoptsub  21174  cnmpt21  21191  elqtop  21217  tgqtop  21232  r0cld  21258  elfg  21392  fbasrn  21405  trfil2  21408  trfil3  21409  fin1aufil  21453  elfm2  21469  elfm3  21471  flimopn  21496  fbflim  21497  flfnei  21512  flftg  21517  cnpflf2  21521  txflf  21527  fclsbas  21542  alexsubALTlem4  21571  cnextfvval  21586  snclseqg  21636  tgphaus  21637  tsmsfbas  21648  tsmssubm  21663  utopsnneip  21769  prdsxmetlem  21889  imasdsf1olem  21894  xpsdsval  21902  blres  21952  isxms2  21969  metcnp  22062  txmetcnp  22068  txmetcn  22069  metustel  22071  metuel2  22086  dscopn  22094  isngp4  22131  cnblcld  22301  metnrmlem1a  22381  metnrmlem1aOLD  22396  icoopnst  22473  iocopnst  22474  elpi1  22580  lmmbr2  22733  cfil3i  22743  caucfil  22757  iscmet3  22767  lmclim  22776  metcld2  22780  bcthlem4  22799  minveclem3b  22874  minveclem6  22880  minveclem7  22881  minveclem3bOLD  22886  minveclem6OLD  22892  minveclem7OLD  22893  ivthle  22911  ivthle2  22912  evthicc2  22915  ovolfioo  22922  ovolficc  22923  ovolgelb  22934  dyadmax  23051  subopnmbl  23057  ismbf3d  23106  mbfimaopnlem  23107  mbfimaopn2  23109  mbfaddlem  23112  mbfsup  23116  mbfinf  23117  i1f1lem  23141  i1fmulclem  23154  itg1climres  23166  mbfi1fseqlem4  23170  itg2monolem1  23202  itg2gt0  23212  isibl  23217  iblcnlem1  23239  ellimc2  23326  dvcnvrelem1  23463  itgsubst  23495  mdegleb  23507  fta1glem2  23611  quotval  23739  vieta1lem1  23757  vieta1lem2  23758  ulm2  23834  ulmcaulem  23843  ulmcau  23844  radcnvlt1  23867  sineq0  23968  cos11  23974  recosf1o  23976  efopn  24095  cxpeq  24189  mcubic  24265  birthdaylem3  24371  rlimcnp  24383  xrlimcnp  24386  eldmgm  24439  dmgmaddn0  24440  lgamgulmlem6  24451  wilth  24488  isppw  24533  isppw2  24534  mumullem2  24599  sqff1o  24601  dvdsmulf1o  24613  fsumvma  24631  fsumvma2  24632  vmasum  24634  chpchtsum  24637  lgsne0  24753  gausslemma2dlem0i  24782  gausslemma2dlem1a  24783  lgseisenlem2  24794  lgsquadlem1  24798  lgsquadlem2  24799  2lgslem1a  24809  dchrmusumlema  24875  rpvmasum2  24894  dchrisum0lema  24896  pntibndlem3  24974  pntlemi  24986  pntleml  24993  pnt3  24994  trgcgrg  25104  tgcgr4  25120  colcom  25147  colrot1  25148  ltgov  25186  hlcomb  25192  lncom  25211  mirreu3  25243  isperp  25301  perpcom  25302  brbtwn  25473  brcgr  25474  brbtwn2  25479  colinearalg  25484  axeuclidlem  25536  axcontlem2  25539  axcontlem4  25541  axcontlem7  25544  nbgraf1olem1  25712  nbgraf1olem5  25716  nbcusgra  25734  uvtx01vtx  25762  cusgrauvtxb  25766  iswlk  25790  istrl  25809  ispth  25840  isspth  25841  wlkdvspthlem  25879  usgrcyclnl2  25911  wwlkn0s  25975  wwlkextwrd  25998  wwlkextproplem3  26013  isclwlk0  26024  clwwlkn2  26045  eclclwwlkn1  26101  eleclclwwlkn  26102  hashecclwwlkn1  26103  usghashecclwwlk  26104  clwlkfclwwlk1hashn  26110  clwlkfoclwwlk  26114  usg2spthonot  26157  isrgra  26195  isrusgra  26196  isrusgusrg  26201  eupath2  26249  frgra3vlem2  26270  frgrancvvdeqlem2  26300  frgrancvvdeqlem3  26301  frgrancvvdeqlemC  26308  usg2spot2nb  26334  isvclem  26574  isnvlem  26609  isphg  26838  isph  26843  phoeqi  26879  ubthlem3  26894  minvecolem5  26903  minvecolem6  26904  minvecolem7  26905  minvecolem5OLD  26913  minvecolem6OLD  26914  minvecolem7OLD  26915  hhph  27211  issh3  27252  nmopub  27943  nmfnleub  27960  adjeq  27970  adjvalval  27972  elunop2  28048  lnophm  28054  nmcexi  28061  cnlnadjlem5  28106  cnlnadjeui  28112  adjbd1o  28120  jpi  28305  mddmd2  28344  chrelati  28399  chrelat2i  28400  cvexchlem  28403  dmdbr5ati  28457  cdjreui  28467  cdj3i  28476  iunxsngf  28550  disjunsn  28581  opeldifid  28586  fcoinvbr  28591  brabgaf  28592  opabdm  28595  opabrn  28596  iunsnima  28600  abfmpunirn  28624  fmptcof2  28631  funcnvmptOLD  28642  funcnvmpt  28643  funcnv5mpt  28644  f1od2  28679  resf1o  28685  fpwrelmap  28688  iocinioc2  28730  eliccioo  28769  posrasymb  28787  isslmd  28886  smatrcl  28990  pstmxmet  29068  prsdm  29088  prsrn  29089  ordtconlem1  29098  xrmulc1cn  29104  ispisys2  29343  elcarsg  29504  eulerpartlemmf  29575  isrrvv  29643  bnj976  29951  bnj944  30111  bnj1173  30173  bnj1321  30198  bnj1373  30201  bnj1417  30212  subfacp1lem3  30267  subfacp1lem6  30270  subfacp1  30271  txpcon  30317  sconpi1  30324  rescon  30331  cvmscbv  30343  cvmsval  30351  cvmlift2lem13  30400  cvmlift3lem2  30405  cvmlift3  30413  mclsrcl  30561  br8  30745  br6  30746  br4  30747  fv1stcnv  30771  fv2ndcnv  30772  distel  30799  poseq  30840  wsuclem  30857  sltsolem1  30906  imageval  31046  funpartfv  31061  dfrdg4  31067  altopthg  31083  altopthbg  31084  brcolinear2  31174  lineext  31192  brsegle  31224  seglelin  31232  broutsideof2  31238  isfne4  31343  isfne2  31345  isfne3  31346  fneval  31355  topfneec  31358  neibastop2lem  31363  neibastop2  31364  neifg  31374  filnetlem4  31384  onsuct0  31448  bj-abbi  31808  bj-tagcg  32001  bj-projval  32012  bj-restuni  32066  csbwrecsg  32184  csboprabg  32187  csbmpt22g  32188  topdifinffinlem  32206  isbasisrelowllem1  32214  isbasisrelowllem2  32215  rdgeqoa  32229  csbfinxpg  32236  wl-sbrimt  32404  wl-sblimt  32405  wl-sbnf1  32409  wl-mo2df  32425  wl-eudf  32427  wl-mo2t  32430  wl-mo3t  32431  wl-ax11-lem6  32440  uncov  32454  tan2h  32465  matunitlindf  32471  ptrest  32472  poimirlem2  32475  poimirlem16  32489  poimirlem19  32492  poimirlem23  32496  poimirlem24  32497  poimirlem25  32498  poimirlem26  32499  poimirlem27  32500  mbfposadd  32521  cnambfre  32522  itg2addnclem2  32526  fdc  32605  heibor1  32673  rrncmslem  32695  rrnheibor  32700  opidonOLD  32715  issmgrpOLD  32726  ismndo  32735  isrngo  32760  isdivrngo  32813  isfldidl2  32932  isdmn3  32937  prtlem13  33065  prter3  33079  lrelat  33213  islshpat  33216  lshpsmreu  33308  lkrpssN  33362  cmtvalN  33410  omllaw2N  33443  cvrval  33468  cvrval2  33473  cvlsupr3  33543  3dim0  33655  islln2  33709  islpln5  33733  islpln2  33734  islpln2ah  33747  islvol5  33777  islvol2  33778  4atlem11  33807  pmapglbx  33967  cdleme18d  34494  cdlemefrs29bpre0  34596  cdlemb3  34806  cdlemg33b  34907  cdlemkid3N  35133  cdlemkid4  35134  dvhb1dimN  35186  dia11N  35249  cdlemm10N  35319  dib11N  35361  dib1dim  35366  dibglbN  35367  diblsmopel  35372  dihopelvalcpre  35449  dih11  35466  dihmeetlem4preN  35507  dihmeetlem13N  35520  lcfrvalsnN  35742  lcfrlem9  35751  lcf1o  35752  mapdval4N  35833  baerlem3lem2  35911  baerlem5alem2  35912  baerlem5blem2  35913  hdmap1fval  35998  hdmapfval  36031  hdmapglem7a  36131  hlhillcs  36162  ellz1  36242  lzunuz  36243  fz1eqin  36244  diophrex  36251  rexrabdioph  36270  rexfrabdioph  36271  2rexfrabdioph  36272  3rexfrabdioph  36273  4rexfrabdioph  36274  6rexfrabdioph  36275  7rexfrabdioph  36276  fzneg  36461  expdioph  36502  wepwsolem  36524  fnwe2lem2  36533  islmodfg  36551  kercvrlsm  36565  sdrgacs  36691  cnvcnvintabd  36826  iunrelexpuztr  36931  brtrclfv2  36939  frege124d  36973  rcompleq  37239  or3or  37240  uneqsn  37242  clsk1independent  37265  ntrclsneine0lem  37283  ntrclsiso  37286  ntrclsk2  37287  ntrclskb  37288  ntrclsk3  37289  ntrclsk13  37290  ntrclsk4  37291  ntrneiel2  37305  ntrneiiso  37310  ntrneikb  37313  ntrneik3  37315  ntrneix3  37316  ntrneik13  37317  ntrneix13  37318  ntrneik4w  37319  k0004lem3  37368  pm10.52  37487  iotasbc  37543  pm14.122a  37546  pm14.122b  37547  pm14.123a  37549  rusbcALT  37563  fvsb  37578  trsbc  37672  rexsngf  38147  iunxsngf2  38157  mapsnd  38285  limcperiod  38598  limsupre  38611  limsupreOLD  38612  dvbdfbdioo  38724  stoweidlem34  38834  fourierdlem108  39016  fourierdlem110  39018  etransc  39087  2reu4a  39749  funressnfv  39768  dfafn5a  39801  el1fzopredsuc  39860  iccelpart  39883  lighneallem2  39973  dfeven2  40012  gboge7  40097  bgoldbwt  40111  riotaeqimp  40272  elfz2z  40286  isuhgr  40391  isushgr  40392  isupgr  40419  isumgr  40429  isuspgr  40491  isusgr  40492  uhgr0v0e  40573  isfusgrf1  40648  opfusgr  40651  usgr1v0e  40654  nbuhgr2vtx1edgb  40683  edgnbusgreu  40704  nbusgredgeu0  40705  isuvtxa  40730  cusgruvtxb  40753  cplgr3v  40766  cusgrsizeinds  40777  vtxdg0v  40797  vtxd0nedgb  40812  vtxduhgr0nedg  40816  vtxdusgr0edgnelALT  40820  is1wlk  40922  isWlk  40923  1wlk1walk  40952  upgr2wlk  40985  usgr2pthlem  41078  isclWlke  41093  isclWlkupgr  41094  iswwlksnx  41151  wwlksnextwrd  41212  wwlksnextproplem3  41226  umgr2wlk  41265  elwwlks2  41279  elwspths2spth  41280  clwlkclwwlk  41320  clwwlksn2  41326  eclclwwlksn1  41368  eleclclwwlksn  41369  hashecclwwlksn1  41370  umgrhashecclwwlk  41371  clwlksfclwwlk1hashn  41375  clwlksfoclwwlk  41379  clwwlksnun  41390  1pthon2v-av  41429  uhgr3cyclex  41458  isconngr  41465  isconngr1  41466  eupth2lems  41515  isfrgr  41539  frgr0v  41542  frgr3vlem2  41553  frgrncvvdeqlem2  41579  frgrncvvdeqlem3  41580  frgrncvvdeqlemC  41587  fusgr2wsp2nb  41607  ismhm0  41704  inclfusubc  41766  isrnghm  41791  rnghmval2  41794  uzlidlring  41828  lidldomnnring  41829  zrninitoringc  41972  opeliun2xp  42013  snlindsntor  42163  elbigo2  42253  gte-lte  42334  gt-lt  42335
  Copyright terms: Public domain W3C validator