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  1023  cad0  1553  ax12wdemo  2009  sbal2  2460  necon3abid  2826  necon3bid  2834  ralxpxfr2d  3311  ceqsrexv  3319  ceqsrex2v  3321  elab2g  3336  elrabf  3343  elrab3t  3345  eueq2  3362  eqreu  3380  reu8  3384  ru  3416  sbcralt  3492  sbcabel  3498  sbcel1g  3959  sbcel2  3961  csbnestgf  3968  sbccsb2  3977  disjpss  4000  sbcssg  4057  rexsng  4190  ralprg  4205  rexprg  4206  difsn  4297  preq2b  4346  opthpr  4352  preqsnd  4360  csbopg  4388  ralunsn  4390  csbuni  4432  dfiin2g  4519  iunxsng  4568  elpwuni  4579  disjxun  4611  sbcbr12g  4668  pwnss  4790  opthneg  4910  otthg  4914  opelopabt  4947  opelopabga  4948  brabga  4949  opelopabgf  4955  csbmpt12  4970  rbropapd  4975  dfid3  4990  frirr  5051  wereu2  5071  brab2a  5129  opeliunxp  5131  posn  5148  sosn  5149  frsn  5150  brab2ga  5155  opbrop  5159  csbcnvgALT  5267  elrnmpt1  5334  elrnmptg  5335  eliniseg2  5464  poleloe  5486  xpdifid  5521  cnvpo  5632  elpred  5652  ordtri4  5720  oneqmini  5735  elsucg  5751  elsuc2g  5752  sbcfung  5871  dffun8  5875  fncnv  5920  fununi  5922  fnssresb  5961  fnimaeq0  5970  csbfv12  6188  dffn5  6198  funimass4  6204  feqmptdf  6208  fnsnfv  6215  dmfco  6229  fndmdif  6277  fvimacnvi  6287  fvimacnvALT  6292  unpreima  6297  respreima  6300  fmptco  6351  fressnfv  6381  fmptsnd  6389  fnnfpeq0  6398  tpres  6420  elunirn  6463  dff13  6466  f12dfv  6483  f13dfv  6484  fliftel  6513  isoini  6542  f1oiso  6555  riotaeqimp  6588  eloprabga  6700  resoprab2  6710  elrnmpt2res  6727  ralrnmpt2  6728  ovid  6730  ov  6733  ovg  6752  ofrfval2  6868  dfwe2  6928  ssonprc  6939  ordpwsuc  6962  dfom2  7014  f1oweALT  7097  el2xptp0  7157  fmpt2x  7181  ovmptss  7203  1stconst  7210  2ndconst  7211  fnsuppres  7267  brtpos2  7303  mpt2curryd  7340  dfsmo2  7389  rdglim2  7473  seqomlem2  7491  omeu  7610  oeeui  7627  brdifun  7716  eqerlem  7721  brecop  7785  erovlem  7788  eceqoveq  7798  mapsn  7843  ixpsnval  7855  mptelixpg  7889  map1  7980  xpsnen  7988  xpdom2  7999  omxpenlem  8005  xpf1o  8066  mapunen  8073  onfin  8095  fimaxg  8151  fodomfib  8184  fofinf1o  8185  fipreima  8216  supub  8309  infglb  8340  infglbb  8341  fiming  8348  fiinfg  8349  ordtypecbv  8366  ordtypelem3  8369  ordtypelem9  8375  hartogslem1  8391  wofib  8394  wemapsolem  8399  wemapso2lem  8401  noinfep  8501  cantnf  8534  rankbnd2  8676  domtri2  8759  infxpenc2  8789  fseqdom  8793  acni2  8813  dfac9  8902  cfeq0  9022  cfsuc  9023  cflim3  9028  cfslb  9032  cofsmo  9035  enfin2i  9087  isfin3ds  9095  isf33lem  9132  fin1a2lem5  9170  axdc2lem  9214  zorn2g  9269  fodomb  9292  brdom7disj  9297  brdom6disj  9298  iundom2g  9306  cfpwsdom  9350  elgch  9388  fpwwe2cbv  9396  fpwwecbv  9410  pwfseqlem3  9426  pwfseqlem4a  9427  pwfseqlem4  9428  ltpiord  9653  nlt1pi  9672  nqereu  9695  addclprlem1  9782  1idpr  9795  reclem3pr  9815  ltsosr  9859  map2psrpr  9875  supsrlem  9876  axrrecex  9928  xrlenlt  10047  eqlei2  10092  addsubeq4  10240  renegcli  10286  lesub0  10489  wloglei  10504  conjmul  10686  rereccl  10687  infm3  10926  supaddc  10934  supadd  10935  supmul1  10936  supmullem1  10937  supmullem2  10938  supmul  10939  creui  10959  nndiv  11005  elznn0  11336  prime  11402  eqreznegel  11718  zsupss  11721  rebtwnz  11731  negelrp  11808  ltxr  11893  elixx3g  12130  ixxun  12133  ioo0  12142  ico0  12163  ioc0  12164  icc0  12165  difreicc  12246  divelunit  12256  iccf1o  12258  elfz2  12275  fzn  12299  fznn  12350  fzshftral  12369  nelfzo  12416  fzosplitsni  12519  om2uzisoi  12693  rabssnn0fi  12725  mptnn0fsupp  12737  sq11i  12894  hashsdom  13110  fi1uzind  13218  fi1uzindOLD  13224  wrdval  13247  csbwrdg  13273  wrd2ind  13415  s2f1o  13597  cjreb  13797  rexfiuz  14021  cau3lem  14028  rlim2  14161  ello12  14181  ello1mpt  14186  elo12  14192  o1lo1  14202  lo1resb  14229  o1resb  14231  o1compt  14252  caucvgb  14344  pwm1geoser  14525  mertens  14543  ruclem12  14895  divides  14909  dvdsabseq  14959  odd2np1  14989  oddm1even  14991  sumodd  15035  divalgmod  15053  modremain  15056  sadadd2lem2  15096  gcdcllem2  15146  bezoutlem2  15181  bezoutlem3  15182  bezoutlem4  15183  isprm2  15319  isprm3  15320  dvdsnprmd  15327  oddprmdvds  15531  prmreclem2  15545  prmreclem5  15548  prmreclem6  15549  4sqlem2  15577  4sqlem12  15584  vdwmc  15606  vdwpc  15608  vdwlem6  15614  vdwlem10  15618  vdwnn  15626  ramval  15636  0ram  15648  prdsleval  16058  pwsle  16073  imasleval  16122  xpsfrnel2  16146  xpsle  16162  isacs2  16235  mreacs  16240  acsfn  16241  iscatd2  16263  catpropd  16290  ciclcl  16383  cicrcl  16384  isssc  16401  evlfcl  16783  uncfcurf  16800  pltval  16881  lublecllem  16909  tosso  16957  oduleg  17053  oduclatb  17065  posglbmo  17068  isipodrs  17082  odudlatb  17117  gsumvalx  17191  sgrp2rid2  17334  grplmulf1o  17410  grplactcnv  17439  elnmz  17554  eqgid  17567  isghm  17581  ghmeqker  17608  resscntz  17685  symg1bas  17737  pgrpsubgsymgbi  17748  symgfixelq  17774  f1omvdconj  17787  odmulgeq  17895  sylow3lem3  17965  sylow3lem6  17968  efgval2  18058  efgsdm  18064  efgrelexlema  18083  efgcpbllemb  18089  iscyggen2  18204  cyggenod  18207  gsummptfzcl  18289  eldprd  18324  dprdf11  18343  dprddisj2  18359  pgpfac1lem2  18395  pgpfac1  18400  srg1zr  18450  drngid2  18684  issubrg  18701  islmod  18788  aspval2  19266  psrbag  19283  cply1coe0bi  19589  zndvds  19817  znleval  19822  iunocv  19944  pjfval2  19972  pjdm2  19974  dsmmelbas  20002  ellspd  20060  islindf  20070  islindf4  20096  istopg  20625  basgen2  20704  isclo  20801  mretopd  20806  isnei  20817  isperf3  20867  restdis  20892  neitr  20894  restcls  20895  restlp  20897  restperf  20898  iscn  20949  iscnp  20951  lmbr2  20973  lmbrf  20974  ordtt1  21093  cmpsub  21113  hauscmplem  21119  cmpfi  21121  dfconn2  21132  1stcelcls  21174  1stccn  21176  nllyi  21188  subislly  21194  dissnlocfin  21242  elkgen  21249  ptpjpre1  21284  ptuni2  21289  ptclsg  21328  ptcnplem  21334  txcn  21339  hausdiag  21358  txhaus  21360  txkgen  21365  xkoptsub  21367  cnmpt21  21384  elqtop  21410  tgqtop  21425  r0cld  21451  elfg  21585  fbasrn  21598  trfil2  21601  trfil3  21602  fin1aufil  21646  elfm2  21662  elfm3  21664  flimopn  21689  fbflim  21690  flfnei  21705  flftg  21710  cnpflf2  21714  txflf  21720  fclsbas  21735  alexsubALTlem4  21764  cnextfvval  21779  snclseqg  21829  tgphaus  21830  tsmsfbas  21841  tsmssubm  21856  utopsnneip  21962  prdsxmetlem  22083  imasdsf1olem  22088  xpsdsval  22096  blres  22146  isxms2  22163  metcnp  22256  txmetcnp  22262  txmetcn  22263  metustel  22265  metuel2  22280  dscopn  22288  isngp4  22326  cnblcld  22488  metnrmlem1a  22569  icoopnst  22646  iocopnst  22647  elpi1  22753  isclmp  22805  isncvsngp  22857  lmmbr2  22965  cfil3i  22975  caucfil  22989  iscmet3  22999  lmclim  23009  metcld2  23013  bcthlem4  23032  minveclem3b  23107  minveclem6  23113  minveclem7  23114  ivthle  23132  ivthle2  23133  evthicc2  23136  ovolfioo  23143  ovolficc  23144  ovolgelb  23155  dyadmax  23272  subopnmbl  23278  ismbf3d  23327  mbfimaopnlem  23328  mbfimaopn2  23330  mbfaddlem  23333  mbfsup  23337  mbfinf  23338  i1f1lem  23362  i1fmulclem  23375  itg1climres  23387  mbfi1fseqlem4  23391  itg2monolem1  23423  itg2gt0  23433  isibl  23438  iblcnlem1  23460  ellimc2  23547  dvcnvrelem1  23684  itgsubst  23716  mdegleb  23728  fta1glem2  23830  quotval  23951  vieta1lem1  23969  vieta1lem2  23970  ulm2  24043  ulmcaulem  24052  ulmcau  24053  radcnvlt1  24076  sineq0  24177  cos11  24183  recosf1o  24185  efopn  24304  cxpeq  24398  mcubic  24474  birthdaylem3  24580  rlimcnp  24592  xrlimcnp  24595  eldmgm  24648  dmgmaddn0  24649  lgamgulmlem6  24660  wilth  24697  isppw  24740  isppw2  24741  mumullem2  24806  sqff1o  24808  dvdsmulf1o  24820  fsumvma  24838  fsumvma2  24839  vmasum  24841  chpchtsum  24844  lgsne0  24960  gausslemma2dlem0i  24989  gausslemma2dlem1a  24990  lgseisenlem2  25001  lgsquadlem1  25005  lgsquadlem2  25006  2lgslem1a  25016  dchrmusumlema  25082  rpvmasum2  25101  dchrisum0lema  25103  pntibndlem3  25181  pntlemi  25193  pntleml  25200  pnt3  25201  trgcgrg  25310  tgcgr4  25326  colcom  25353  colrot1  25354  ltgov  25392  hlcomb  25398  lncom  25417  mirreu3  25449  isperp  25507  perpcom  25508  brbtwn  25679  brcgr  25680  brbtwn2  25685  colinearalg  25690  axeuclidlem  25742  axcontlem2  25745  axcontlem4  25747  axcontlem7  25750  isuhgr  25851  isushgr  25852  isupgr  25875  isumgr  25885  isuspgr  25940  isusgr  25941  uhgr0v0e  26023  isfusgrf1  26100  opfusgr  26103  usgr1v0e  26106  nbuhgr2vtx1edgb  26135  edgnbusgreu  26156  nbusgredgeu0  26157  isuvtxa  26182  cusgruvtxb  26205  cplgr3v  26218  cusgrsizeinds  26235  vtxdg0v  26255  vtxd0nedgb  26270  vtxduhgr0nedg  26274  vtxdusgr0edgnelALT  26278  iswlk  26376  wlk1walk  26404  upgr2wlk  26433  upgristrl  26468  2pthnloop  26496  usgr2pthlem  26528  isclwlke  26542  isclwlkupgr  26543  iswwlksnx  26600  wwlksnextwrd  26661  wwlksnextproplem3  26675  umgr2wlk  26714  elwwlks2  26728  elwspths2spth  26729  clwlkclwwlk  26770  clwwlksn2  26776  eclclwwlksn1  26818  eleclclwwlksn  26819  hashecclwwlksn1  26820  umgrhashecclwwlk  26821  clwlksfclwwlk1hashn  26825  clwlksfoclwwlk  26829  clwwlksnun  26840  1pthon2v  26879  uhgr3cyclex  26908  isconngr  26915  isconngr1  26916  eupthres  26941  eupth2lems  26964  isfrgr  26988  frgr0v  26991  frgr3vlem2  27002  frgrncvvdeqlem2  27028  frgrncvvdeqlem3  27029  frgrncvvdeqlemC  27036  fusgr2wsp2nb  27056  isvclem  27281  isnvlem  27314  isphg  27521  isph  27526  phoeqi  27562  ubthlem3  27577  minvecolem5  27586  minvecolem6  27587  minvecolem7  27588  hhph  27884  issh3  27925  nmopub  28616  nmfnleub  28633  adjeq  28643  adjvalval  28645  elunop2  28721  lnophm  28727  nmcexi  28734  cnlnadjlem5  28779  cnlnadjeui  28785  adjbd1o  28793  jpi  28978  mddmd2  29017  chrelati  29072  chrelat2i  29073  cvexchlem  29076  dmdbr5ati  29130  cdjreui  29140  cdj3i  29149  iunxsngf  29221  disjunsn  29252  opeldifid  29257  fcoinvbr  29262  brabgaf  29263  opabdm  29266  opabrn  29267  iunsnima  29271  abfmpunirn  29294  fmptcof2  29299  funcnvmptOLD  29310  funcnvmpt  29311  funcnv5mpt  29312  f1od2  29342  resf1o  29348  fpwrelmap  29351  iocinioc2  29385  eliccioo  29424  posrasymb  29442  isslmd  29540  smatrcl  29644  pstmxmet  29722  prsdm  29742  prsrn  29743  ordtconnlem1  29752  xrmulc1cn  29758  ispisys2  29997  elcarsg  30148  eulerpartlemmf  30218  isrrvv  30286  bnj976  30556  bnj944  30716  bnj1173  30778  bnj1321  30803  bnj1373  30806  bnj1417  30817  subfacp1lem3  30872  subfacp1lem6  30875  subfacp1  30876  txpconn  30922  sconnpi1  30929  resconn  30936  cvmscbv  30948  cvmsval  30956  cvmlift2lem13  31005  cvmlift3lem2  31010  cvmlift3  31018  mclsrcl  31166  br8  31354  br6  31355  br4  31356  fv1stcnv  31382  fv2ndcnv  31383  distel  31410  poseq  31451  wsuclem  31474  wsuclemOLD  31475  sltsolem1  31528  imageval  31679  funpartfv  31694  dfrdg4  31700  altopthg  31716  altopthbg  31717  brcolinear2  31807  lineext  31825  brsegle  31857  seglelin  31865  broutsideof2  31871  isfne4  31977  isfne2  31979  isfne3  31980  fneval  31989  topfneec  31992  neibastop2lem  31997  neibastop2  31998  neifg  32008  filnetlem4  32018  onsuct0  32082  bj-abbi  32418  bj-tagcg  32620  bj-projval  32631  bj-restuni  32687  csbwrecsg  32805  csboprabg  32808  csbmpt22g  32809  topdifinffinlem  32827  isbasisrelowllem1  32835  isbasisrelowllem2  32836  rdgeqoa  32850  csbfinxpg  32857  wl-sbrimt  32963  wl-sblimt  32964  wl-sbnf1  32968  wl-mo2df  32984  wl-eudf  32986  wl-mo2t  32989  wl-mo3t  32990  wl-ax11-lem6  32999  uncov  33022  tan2h  33033  matunitlindf  33039  ptrest  33040  poimirlem2  33043  poimirlem16  33057  poimirlem19  33060  poimirlem23  33064  poimirlem24  33065  poimirlem25  33066  poimirlem26  33067  poimirlem27  33068  mbfposadd  33089  cnambfre  33090  itg2addnclem2  33094  fdc  33173  heibor1  33241  rrncmslem  33263  rrnheibor  33268  opidonOLD  33283  issmgrpOLD  33294  ismndo  33303  isrngo  33328  isdivrngo  33381  isfldidl2  33500  isdmn3  33505  prtlem13  33633  prter3  33647  lrelat  33781  islshpat  33784  lshpsmreu  33876  lkrpssN  33930  cmtvalN  33978  omllaw2N  34011  cvrval  34036  cvrval2  34041  cvlsupr3  34111  3dim0  34223  islln2  34277  islpln5  34301  islpln2  34302  islpln2ah  34315  islvol5  34345  islvol2  34346  4atlem11  34375  pmapglbx  34535  cdleme18d  35062  cdlemefrs29bpre0  35164  cdlemb3  35374  cdlemg33b  35475  cdlemkid3N  35701  cdlemkid4  35702  dvhb1dimN  35754  dia11N  35817  cdlemm10N  35887  dib11N  35929  dib1dim  35934  dibglbN  35935  diblsmopel  35940  dihopelvalcpre  36017  dih11  36034  dihmeetlem4preN  36075  dihmeetlem13N  36088  lcfrvalsnN  36310  lcfrlem9  36319  lcf1o  36320  mapdval4N  36401  baerlem3lem2  36479  baerlem5alem2  36480  baerlem5blem2  36481  hdmap1fval  36566  hdmapfval  36599  hdmapglem7a  36699  hlhillcs  36730  ellz1  36810  lzunuz  36811  fz1eqin  36812  diophrex  36819  rexrabdioph  36838  rexfrabdioph  36839  2rexfrabdioph  36840  3rexfrabdioph  36841  4rexfrabdioph  36842  6rexfrabdioph  36843  7rexfrabdioph  36844  fzneg  37029  expdioph  37070  wepwsolem  37092  fnwe2lem2  37101  islmodfg  37119  kercvrlsm  37133  sdrgacs  37252  cnvcnvintabd  37387  iunrelexpuztr  37492  brtrclfv2  37500  frege124d  37534  rcompleq  37800  or3or  37801  uneqsn  37803  clsk1independent  37826  ntrclsneine0lem  37844  ntrclsiso  37847  ntrclsk2  37848  ntrclskb  37849  ntrclsk3  37850  ntrclsk13  37851  ntrclsk4  37852  ntrneiel2  37866  ntrneiiso  37871  ntrneikb  37874  ntrneik3  37876  ntrneix3  37877  ntrneik13  37878  ntrneix13  37879  ntrneik4w  37880  k0004lem3  37929  pm10.52  38046  iotasbc  38102  pm14.122a  38105  pm14.122b  38106  pm14.123a  38108  rusbcALT  38122  fvsb  38138  trsbc  38232  rexsngf  38705  iunxsngf2  38715  mapsnd  38862  limcperiod  39264  limsupre  39277  dvbdfbdioo  39451  stoweidlem34  39558  fourierdlem108  39738  fourierdlem110  39740  etransc  39807  2reu4a  40493  funressnfv  40512  dfafn5a  40544  elfz2z  40622  el1fzopredsuc  40632  iccelpart  40667  lighneallem2  40822  dfeven2  40861  gboge7  40946  bgoldbwt  40960  isupwlk  41005  uspgrsprfo  41044  ismhm0  41093  inclfusubc  41155  isrnghm  41180  rnghmval2  41183  uzlidlring  41217  lidldomnnring  41218  zrninitoringc  41359  opeliun2xp  41399  snlindsntor  41548  elbigo2  41638  gte-lte  41758  gt-lt  41759
  Copyright terms: Public domain W3C validator