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

Theorem syl5bb 272
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 268 1 (𝜒 → (𝜑𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
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 197
This theorem is referenced by:  syl5rbb  273  syl5bbr  274  3bitr4g  303  imim21b  382  ifpfal  1024  cad0  1555  ax12wdemo  2011  sbal2  2460  necon3abid  2829  necon3bid  2837  ralxpxfr2d  3325  ceqsrexv  3334  ceqsrex2v  3336  elab2g  3351  elrabf  3358  elrab3t  3360  eueq2  3378  eqreu  3396  reu8  3400  ru  3432  sbcralt  3508  sbcabel  3515  sbcel1g  3985  sbcel2  3987  csbnestgf  3994  sbccsb2  4003  disjpss  4026  sbcssg  4083  rexsng  4217  ralprg  4232  rexprg  4233  difsn  4326  preq2b  4376  opthpr  4382  preqsnd  4390  csbopg  4418  ralunsn  4420  csbuni  4464  dfiin2g  4551  iunxsng  4600  elpwuni  4614  disjxun  4649  sbcbr12g  4706  pwnss  4828  opthneg  4948  otthg  4952  opelopabt  4985  opelopabga  4986  brabga  4987  opelopabgf  4993  csbmpt12  5008  rbropapd  5013  dfid3  5023  frirr  5089  wereu2  5109  opeliunxp  5168  posn  5185  sosn  5186  frsn  5187  brab2a  5192  opbrop  5196  csbcnvgALT  5305  elrnmpt1  5372  elrnmptg  5373  eliniseg2  5503  poleloe  5525  xpdifid  5560  cnvpo  5671  elpred  5691  ordtri4  5759  oneqmini  5774  elsucg  5790  elsuc2g  5791  sbcfung  5910  dffun8  5914  fncnv  5960  fununi  5962  fnssresb  6001  fnimaeq0  6011  csbfv12  6229  dffn5  6239  funimass4  6245  feqmptdf  6249  fnsnfv  6256  dmfco  6270  fndmdif  6319  fvimacnvi  6329  fvimacnvALT  6334  unpreima  6339  respreima  6342  fmptco  6394  fressnfv  6424  fmptsnd  6432  fnnfpeq0  6441  tpres  6463  elunirn  6506  dff13  6509  f12dfv  6526  f13dfv  6527  fliftel  6556  isoini  6585  f1oiso  6598  riotaeqimp  6631  eloprabga  6744  resoprab2  6754  elrnmpt2res  6771  ralrnmpt2  6772  ovid  6774  ov  6777  ovg  6796  ofrfval2  6912  dfwe2  6978  ssonprc  6989  ordpwsuc  7012  dfom2  7064  f1oweALT  7149  el2xptp0  7209  fmpt2x  7233  ovmptss  7255  1stconst  7262  2ndconst  7263  fnsuppres  7319  brtpos2  7355  mpt2curryd  7392  dfsmo2  7441  rdglim2  7525  seqomlem2  7543  omeu  7662  oeeui  7679  brdifun  7768  eqerlem  7773  brecop  7837  erovlem  7840  eceqoveq  7850  mapsn  7896  ixpsnval  7908  mptelixpg  7942  map1  8033  xpsnen  8041  xpdom2  8052  omxpenlem  8058  xpf1o  8119  mapunen  8126  onfin  8148  fimaxg  8204  fodomfib  8237  fofinf1o  8238  fipreima  8269  supub  8362  infglb  8393  infglbb  8394  fiming  8401  fiinfg  8402  ordtypecbv  8419  ordtypelem3  8422  ordtypelem9  8428  hartogslem1  8444  wofib  8447  wemapsolem  8452  wemapso2lem  8454  noinfep  8554  cantnf  8587  rankbnd2  8729  domtri2  8812  infxpenc2  8842  fseqdom  8846  acni2  8866  dfac9  8955  cfeq0  9075  cfsuc  9076  cflim3  9081  cfslb  9085  cofsmo  9088  enfin2i  9140  isfin3ds  9148  isf33lem  9185  fin1a2lem5  9223  axdc2lem  9267  zorn2g  9322  fodomb  9345  brdom7disj  9350  brdom6disj  9351  iundom2g  9359  cfpwsdom  9403  elgch  9441  fpwwe2cbv  9449  fpwwecbv  9463  pwfseqlem3  9479  pwfseqlem4a  9480  pwfseqlem4  9481  ltpiord  9706  nlt1pi  9725  nqereu  9748  addclprlem1  9835  1idpr  9848  reclem3pr  9868  ltsosr  9912  map2psrpr  9928  supsrlem  9929  axrrecex  9981  xrlenlt  10100  eqlei2  10145  addsubeq4  10293  renegcli  10339  lesub0  10542  wloglei  10557  conjmul  10739  rereccl  10740  infm3  10979  supaddc  10987  supadd  10988  supmul1  10989  supmullem1  10990  supmullem2  10991  supmul  10992  creui  11012  nndiv  11058  elznn0  11389  prime  11455  eqreznegel  11771  zsupss  11774  rebtwnz  11784  negelrp  11861  ltxr  11946  elixx3g  12185  ixxun  12188  ioo0  12197  ico0  12218  ioc0  12219  icc0  12220  difreicc  12301  divelunit  12311  iccf1o  12313  elfz2  12330  fzn  12354  fznn  12405  fzshftral  12424  nelfzo  12471  fzosplitsni  12574  om2uzisoi  12748  rabssnn0fi  12780  mptnn0fsupp  12792  sq11i  12949  hashsdom  13165  fi1uzind  13274  fi1uzindOLD  13280  wrdval  13303  csbwrdg  13329  wrd2ind  13471  s2f1o  13655  cjreb  13857  rexfiuz  14081  cau3lem  14088  rlim2  14221  ello12  14241  ello1mpt  14246  elo12  14252  o1lo1  14262  lo1resb  14289  o1resb  14291  o1compt  14312  caucvgb  14404  pwm1geoser  14594  mertens  14612  ruclem12  14964  divides  14979  dvdsabseq  15029  odd2np1  15059  oddm1even  15061  sumodd  15105  divalgmod  15123  modremain  15126  sadadd2lem2  15166  gcdcllem2  15216  bezoutlem2  15251  bezoutlem3  15252  bezoutlem4  15253  isprm2  15389  isprm3  15390  dvdsnprmd  15397  oddprmdvds  15601  prmreclem2  15615  prmreclem5  15618  prmreclem6  15619  4sqlem2  15647  4sqlem12  15654  vdwmc  15676  vdwpc  15678  vdwlem6  15684  vdwlem10  15688  vdwnn  15696  ramval  15706  0ram  15718  prdsleval  16131  pwsle  16146  imasleval  16195  xpsfrnel2  16219  xpsle  16235  isacs2  16308  mreacs  16313  acsfn  16314  iscatd2  16336  catpropd  16363  ciclcl  16456  cicrcl  16457  isssc  16474  evlfcl  16856  uncfcurf  16873  pltval  16954  lublecllem  16982  tosso  17030  oduleg  17126  oduclatb  17138  posglbmo  17141  isipodrs  17155  odudlatb  17190  gsumvalx  17264  sgrp2rid2  17407  grplmulf1o  17483  grplactcnv  17512  elnmz  17627  eqgid  17640  isghm  17654  ghmeqker  17681  resscntz  17758  symg1bas  17810  pgrpsubgsymgbi  17821  symgfixelq  17847  f1omvdconj  17860  odmulgeq  17968  sylow3lem3  18038  sylow3lem6  18041  efgval2  18131  efgsdm  18137  efgrelexlema  18156  efgcpbllemb  18162  iscyggen2  18277  cyggenod  18280  gsummptfzcl  18362  eldprd  18397  dprdf11  18416  dprddisj2  18432  pgpfac1lem2  18468  pgpfac1  18473  srg1zr  18523  drngid2  18757  issubrg  18774  islmod  18861  aspval2  19341  psrbag  19358  cply1coe0bi  19664  zndvds  19892  znleval  19897  iunocv  20019  pjfval2  20047  pjdm2  20049  dsmmelbas  20077  ellspd  20135  islindf  20145  islindf4  20171  istopg  20694  basgen2  20787  isclo  20885  mretopd  20890  isnei  20901  isperf3  20951  restdis  20976  neitr  20978  restcls  20979  restlp  20981  restperf  20982  iscn  21033  iscnp  21035  lmbr2  21057  lmbrf  21058  ordtt1  21177  cmpsub  21197  hauscmplem  21203  cmpfi  21205  dfconn2  21216  1stcelcls  21258  1stccn  21260  nllyi  21272  subislly  21278  dissnlocfin  21326  elkgen  21333  ptpjpre1  21368  ptuni2  21373  ptclsg  21412  ptcnplem  21418  txcn  21423  hausdiag  21442  txhaus  21444  txkgen  21449  xkoptsub  21451  cnmpt21  21468  elqtop  21494  tgqtop  21509  r0cld  21535  elfg  21669  fbasrn  21682  trfil2  21685  trfil3  21686  fin1aufil  21730  elfm2  21746  elfm3  21748  flimopn  21773  fbflim  21774  flfnei  21789  flftg  21794  cnpflf2  21798  txflf  21804  fclsbas  21819  alexsubALTlem4  21848  cnextfvval  21863  snclseqg  21913  tgphaus  21914  tsmsfbas  21925  tsmssubm  21940  utopsnneip  22046  prdsxmetlem  22167  imasdsf1olem  22172  xpsdsval  22180  blres  22230  isxms2  22247  metcnp  22340  txmetcnp  22346  txmetcn  22347  metustel  22349  metuel2  22364  dscopn  22372  isngp4  22410  cnblcld  22572  metnrmlem1a  22655  icoopnst  22732  iocopnst  22733  elpi1  22839  isclmp  22891  isncvsngp  22943  lmmbr2  23051  cfil3i  23061  caucfil  23075  iscmet3  23085  lmclim  23095  metcld2  23099  bcthlem4  23118  minveclem3b  23193  minveclem6  23199  minveclem7  23200  ivthle  23219  ivthle2  23220  evthicc2  23223  ovolfioo  23230  ovolficc  23231  ovolgelb  23242  dyadmax  23360  subopnmbl  23366  ismbf3d  23415  mbfimaopnlem  23416  mbfimaopn2  23418  mbfaddlem  23421  mbfsup  23425  mbfinf  23426  i1f1lem  23450  i1fmulclem  23463  itg1climres  23475  mbfi1fseqlem4  23479  itg2monolem1  23511  itg2gt0  23521  isibl  23526  iblcnlem1  23548  ellimc2  23635  dvcnvrelem1  23774  itgsubst  23806  mdegleb  23818  fta1glem2  23920  quotval  24041  vieta1lem1  24059  vieta1lem2  24060  ulm2  24133  ulmcaulem  24142  ulmcau  24143  radcnvlt1  24166  sineq0  24267  cos11  24273  recosf1o  24275  efopn  24398  cxpeq  24492  mcubic  24568  birthdaylem3  24674  rlimcnp  24686  xrlimcnp  24689  eldmgm  24742  dmgmaddn0  24743  lgamgulmlem6  24754  wilth  24791  isppw  24834  isppw2  24835  mumullem2  24900  sqff1o  24902  dvdsmulf1o  24914  fsumvma  24932  fsumvma2  24933  vmasum  24935  chpchtsum  24938  lgsne0  25054  gausslemma2dlem0i  25083  gausslemma2dlem1a  25084  lgseisenlem2  25095  lgsquadlem1  25099  lgsquadlem2  25100  2lgslem1a  25110  dchrmusumlema  25176  rpvmasum2  25195  dchrisum0lema  25197  pntibndlem3  25275  pntlemi  25287  pntleml  25294  pnt3  25295  trgcgrg  25404  tgcgr4  25420  colcom  25447  colrot1  25448  ltgov  25486  hlcomb  25492  lncom  25511  mirreu3  25543  isperp  25601  perpcom  25602  brbtwn  25773  brcgr  25774  brbtwn2  25779  colinearalg  25784  axeuclidlem  25836  axcontlem2  25839  axcontlem4  25841  axcontlem7  25844  edgiedgb  25941  isuhgr  25949  isushgr  25950  isupgr  25973  isumgr  25984  isuspgr  26041  isusgr  26042  uhgr0v0e  26124  isfusgrf1  26206  opfusgr  26209  usgr1v0e  26212  dfnbgr3  26230  nbuhgr2vtx1edgb  26242  edgnbusgreu  26263  nbusgredgeu0  26264  isuvtxa  26289  cusgruvtxb  26312  cplgr3v  26325  cusgrsizeinds  26342  vtxdg0v  26363  vtxd0nedgb  26378  vtxduhgr0nedg  26382  vtxdusgr0edgnelALT  26386  iswlk  26500  wlk1walk  26529  upgr2wlk  26558  upgristrl  26593  2pthnloop  26621  usgr2pthlem  26653  isclwlke  26667  isclwlkupgr  26668  iswwlksnx  26725  wwlksnextwrd  26786  wwlksnextproplem3  26800  2pthon3v  26833  umgr2wlk  26839  elwwlks2  26855  elwspths2spth  26856  clwlkclwwlk  26897  clwwlksn2  26903  eclclwwlksn1  26945  eleclclwwlksn  26946  hashecclwwlksn1  26947  umgrhashecclwwlk  26948  clwlksfclwwlk1hashn  26952  clwlksfoclwwlk  26956  clwwlksnun  26967  1pthon2v  27006  uhgr3cyclex  27035  isconngr  27042  isconngr1  27043  eupthres  27068  eupth2lems  27091  isfrgr  27115  frgr0v  27118  frgr3vlem2  27131  fusgr2wsp2nb  27185  isvclem  27416  isnvlem  27449  isphg  27656  isph  27661  phoeqi  27697  ubthlem3  27712  minvecolem5  27721  minvecolem6  27722  minvecolem7  27723  hhph  28019  issh3  28060  nmopub  28751  nmfnleub  28768  adjeq  28778  adjvalval  28780  elunop2  28856  lnophm  28862  nmcexi  28869  cnlnadjlem5  28914  cnlnadjeui  28920  adjbd1o  28928  jpi  29113  mddmd2  29152  chrelati  29207  chrelat2i  29208  cvexchlem  29211  dmdbr5ati  29265  cdjreui  29275  cdj3i  29284  iunxsngf  29359  disjunsn  29391  opeldifid  29396  fcoinvbr  29403  brabgaf  29404  opabdm  29407  opabrn  29408  iunsnima  29412  elimampt  29422  abfmpunirn  29436  fmptcof2  29441  funcnvmptOLD  29452  funcnvmpt  29453  funcnv5mpt  29454  f1od2  29484  resf1o  29490  fpwrelmap  29493  iocinioc2  29526  eliccioo  29624  posrasymb  29642  isslmd  29740  smatrcl  29847  pstmxmet  29925  prsdm  29945  prsrn  29946  ordtconnlem1  29955  xrmulc1cn  29961  ispisys2  30201  elcarsg  30352  eulerpartlemmf  30422  isrrvv  30490  reprinrn  30681  tgoldbachgt  30726  bnj976  30833  bnj944  30993  bnj1173  31055  bnj1321  31080  bnj1373  31083  bnj1417  31094  subfacp1lem3  31149  subfacp1lem6  31152  subfacp1  31153  txpconn  31199  sconnpi1  31206  resconn  31213  cvmscbv  31225  cvmsval  31233  cvmlift2lem13  31282  cvmlift3lem2  31287  cvmlift3  31295  mclsrcl  31443  br8  31632  br6  31633  br4  31634  elintfv  31648  fv1stcnv  31664  fv2ndcnv  31665  distel  31693  poseq  31734  wsuclem  31757  wsuclemOLD  31758  sltsolem1  31810  nosupdm  31834  nosupbnd1lem4  31841  slenlt  31861  sleloe  31863  etasslt  31904  madeval2  31920  imageval  32021  funpartfv  32036  dfrdg4  32042  altopthg  32058  altopthbg  32059  brcolinear2  32149  lineext  32167  brsegle  32199  seglelin  32207  broutsideof2  32213  isfne4  32319  isfne2  32321  isfne3  32322  fneval  32331  topfneec  32334  neibastop2lem  32339  neibastop2  32340  neifg  32350  filnetlem4  32360  onsuct0  32424  bj-abbi  32759  bj-tagcg  32957  bj-projval  32968  bj-restuni  33034  bj-raldifsn  33038  csbwrecsg  33153  csboprabg  33156  csbmpt22g  33157  topdifinffinlem  33175  isbasisrelowllem1  33183  isbasisrelowllem2  33184  rdgeqoa  33198  csbfinxpg  33205  wl-sbrimt  33311  wl-sblimt  33312  wl-sbnf1  33316  wl-mo2df  33332  wl-eudf  33334  wl-mo2t  33337  wl-mo3t  33338  wl-ax11-lem6  33347  uncov  33370  tan2h  33381  matunitlindf  33387  ptrest  33388  poimirlem2  33391  poimirlem16  33405  poimirlem19  33408  poimirlem23  33412  poimirlem24  33413  poimirlem25  33414  poimirlem26  33415  poimirlem27  33416  mbfposadd  33437  cnambfre  33438  itg2addnclem2  33442  fdc  33521  heibor1  33589  rrncmslem  33611  rrnheibor  33616  opidonOLD  33631  issmgrpOLD  33642  ismndo  33651  isrngo  33676  isdivrngo  33729  isfldidl2  33848  isdmn3  33853  prtlem13  33979  prter3  33993  lrelat  34127  islshpat  34130  lshpsmreu  34222  lkrpssN  34276  cmtvalN  34324  omllaw2N  34357  cvrval  34382  cvrval2  34387  cvlsupr3  34457  3dim0  34569  islln2  34623  islpln5  34647  islpln2  34648  islpln2ah  34661  islvol5  34691  islvol2  34692  4atlem11  34721  pmapglbx  34881  cdleme18d  35408  cdlemefrs29bpre0  35510  cdlemb3  35720  cdlemg33b  35821  cdlemkid3N  36047  cdlemkid4  36048  dvhb1dimN  36100  dia11N  36163  cdlemm10N  36233  dib11N  36275  dib1dim  36280  dibglbN  36281  diblsmopel  36286  dihopelvalcpre  36363  dih11  36380  dihmeetlem4preN  36421  dihmeetlem13N  36434  lcfrvalsnN  36656  lcfrlem9  36665  lcf1o  36666  mapdval4N  36747  baerlem3lem2  36825  baerlem5alem2  36826  baerlem5blem2  36827  hdmap1fval  36912  hdmapfval  36945  hdmapglem7a  37045  hlhillcs  37076  ellz1  37156  lzunuz  37157  fz1eqin  37158  diophrex  37165  rexrabdioph  37184  rexfrabdioph  37185  2rexfrabdioph  37186  3rexfrabdioph  37187  4rexfrabdioph  37188  6rexfrabdioph  37189  7rexfrabdioph  37190  fzneg  37375  expdioph  37416  wepwsolem  37438  fnwe2lem2  37447  islmodfg  37465  kercvrlsm  37479  sdrgacs  37597  cnvcnvintabd  37732  iunrelexpuztr  37837  brtrclfv2  37845  frege124d  37879  rcompleq  38144  or3or  38145  uneqsn  38147  clsk1independent  38170  ntrclsneine0lem  38188  ntrclsiso  38191  ntrclsk2  38192  ntrclskb  38193  ntrclsk3  38194  ntrclsk13  38195  ntrclsk4  38196  ntrneiel2  38210  ntrneiiso  38215  ntrneikb  38218  ntrneik3  38220  ntrneix3  38221  ntrneik13  38222  ntrneix13  38223  ntrneik4w  38224  k0004lem3  38273  pm10.52  38390  iotasbc  38446  pm14.122a  38449  pm14.122b  38450  pm14.123a  38452  rusbcALT  38466  fvsb  38482  trsbc  38576  rexsngf  39046  iunxsngf2  39056  mapsnd  39210  limcperiod  39666  limsupre  39679  dvbdfbdioo  39914  stoweidlem34  40020  fourierdlem108  40200  fourierdlem110  40202  etransc  40269  2reu4a  40958  funressnfv  40977  dfafn5a  41009  elfz2z  41094  el1fzopredsuc  41104  iccelpart  41139  lighneallem2  41294  dfeven2  41333  gbowge7  41422  sbgoldbwt  41436  isupwlk  41488  uspgrsprfo  41527  ismhm0  41576  inclfusubc  41638  isrnghm  41663  rnghmval2  41666  uzlidlring  41700  lidldomnnring  41701  zrninitoringc  41842  opeliun2xp  41882  snlindsntor  42031  elbigo2  42117  gte-lte  42236  gt-lt  42237
  Copyright terms: Public domain W3C validator