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  1998  sbal2  2448  necon3abid  2817  necon3bid  2825  ralxpxfr2d  3297  ceqsrexv  3305  ceqsrex2v  3307  elab2g  3321  elrabf  3328  elrab3t  3329  eueq2  3346  eqreu  3364  reu8  3368  ru  3400  sbcralt  3476  sbcabel  3482  sbcel1g  3938  sbcel2  3940  csbnestgf  3947  sbccsb2  3956  disjpss  3979  sbcssg  4034  rexsng  4165  ralprg  4180  rexprg  4181  difsn  4268  preq2b  4313  opthpr  4319  preqsnd  4325  csbopg  4352  ralunsn  4354  csbuni  4396  dfiin2g  4483  iunxsng  4532  elpwuni  4543  disjxun  4575  sbcbr12g  4632  pwnss  4751  opthneg  4870  otthg  4874  opelopabt  4902  opelopabga  4903  brabga  4904  opelopabgf  4910  csbmpt12  4924  rbropapd  4929  dfid3  4944  frirr  5005  wereu2  5025  brab2a  5081  opeliunxp  5083  posn  5100  sosn  5101  frsn  5102  brab2ga  5107  opbrop  5111  csbcnvgALT  5217  elrnmpt1  5282  elrnmptg  5283  eliniseg2  5411  poleloe  5433  xpdifid  5467  cnvpo  5576  elpred  5596  ordtri4  5664  oneqmini  5679  elsucg  5695  elsuc2g  5696  sbcfung  5813  dffun8  5817  fncnv  5862  fununi  5864  fnssresb  5903  fnimaeq0  5912  csbfv12  6126  dffn5  6136  funimass4  6142  feqmptdf  6146  fnsnfv  6153  dmfco  6167  fndmdif  6214  fvimacnvi  6224  fvimacnvALT  6229  unpreima  6234  respreima  6237  fmptco  6288  fressnfv  6310  fmptsnd  6318  fnnfpeq0  6327  tpres  6349  elunirn  6391  dff13  6394  f12dfv  6407  f13dfv  6408  fliftel  6437  isoini  6466  f1oiso  6479  eloprabga  6623  resoprab2  6633  elrnmpt2res  6650  ralrnmpt2  6651  ovid  6653  ov  6656  ovg  6675  ofrfval2  6790  dfwe2  6850  ssonprc  6861  ordpwsuc  6884  dfom2  6936  f1oweALT  7020  el2xptp0  7080  fmpt2x  7102  ovmptss  7122  1stconst  7129  2ndconst  7130  fnsuppres  7186  brtpos2  7222  mpt2curryd  7259  dfsmo2  7308  rdglim2  7392  seqomlem2  7410  omeu  7529  oeeui  7546  brdifun  7635  eqerlem  7640  brecop  7704  erovlem  7707  eceqoveq  7717  mapsn  7762  ixpsnval  7774  mptelixpg  7808  map1  7898  xpsnen  7906  xpdom2  7917  omxpenlem  7923  xpf1o  7984  mapunen  7991  onfin  8013  fimaxg  8069  fodomfib  8102  fofinf1o  8103  fipreima  8132  supub  8225  infglb  8256  infglbb  8257  fiming  8264  fiinfg  8265  ordtypecbv  8282  ordtypelem3  8285  ordtypelem9  8291  hartogslem1  8307  wofib  8310  wemapsolem  8315  wemapso2lem  8317  noinfep  8417  cantnf  8450  rankbnd2  8592  domtri2  8675  infxpenc2  8705  fseqdom  8709  acni2  8729  dfac9  8818  cfeq0  8938  cfsuc  8939  cflim3  8944  cfslb  8948  cofsmo  8951  enfin2i  9003  isfin3ds  9011  isf33lem  9048  fin1a2lem5  9086  axdc2lem  9130  zorn2g  9185  fodomb  9206  brdom7disj  9211  brdom6disj  9212  iundom2g  9218  cfpwsdom  9262  elgch  9300  fpwwe2cbv  9308  fpwwecbv  9322  pwfseqlem3  9338  pwfseqlem4a  9339  pwfseqlem4  9340  ltpiord  9565  nlt1pi  9584  nqereu  9607  addclprlem1  9694  1idpr  9707  reclem3pr  9727  ltsosr  9771  map2psrpr  9787  supsrlem  9788  axrrecex  9840  xrlenlt  9954  eqlei2  9999  addsubeq4  10147  renegcli  10193  lesub0  10394  wloglei  10409  conjmul  10591  rereccl  10592  infm3  10831  supaddc  10837  supadd  10838  supmul1  10839  supmullem1  10840  supmullem2  10841  supmul  10842  creui  10862  nndiv  10908  elznn0  11225  prime  11290  eqreznegel  11606  zsupss  11609  rebtwnz  11619  negelrp  11696  ltxr  11784  elixx3g  12015  ixxun  12018  ioo0  12027  ico0  12048  ioc0  12049  icc0  12050  difreicc  12131  divelunit  12141  iccf1o  12143  elfz2  12159  fzn  12183  fznn  12233  fzshftral  12252  nelfzo  12299  fzosplitsni  12399  om2uzisoi  12570  rabssnn0fi  12602  mptnn0fsupp  12614  sq11i  12771  hashsdom  12983  fi1uzind  13080  fi1uzindOLD  13086  wrdval  13109  csbwrdg  13135  wrd2ind  13275  s2f1o  13457  cjreb  13657  rexfiuz  13881  cau3lem  13888  rlim2  14021  ello12  14041  ello1mpt  14046  elo12  14052  o1lo1  14062  lo1resb  14089  o1resb  14091  o1compt  14112  caucvgb  14204  pwm1geoser  14385  mertens  14403  ruclem12  14755  divides  14769  dvdsabseq  14819  odd2np1  14849  oddm1even  14851  sumodd  14895  divalgmod  14913  modremain  14916  sadadd2lem2  14956  gcdcllem2  15006  bezoutlem2  15041  bezoutlem3  15042  bezoutlem4  15043  isprm2  15179  isprm3  15180  dvdsnprmd  15187  oddprmdvds  15391  prmreclem2  15405  prmreclem5  15408  prmreclem6  15409  4sqlem2  15437  4sqlem12  15444  vdwmc  15466  vdwpc  15468  vdwlem6  15474  vdwlem10  15478  vdwnn  15486  ramval  15496  0ram  15508  prdsleval  15906  pwsle  15921  imasleval  15970  xpsfrnel2  15994  xpsle  16010  isacs2  16083  mreacs  16088  acsfn  16089  iscatd2  16111  catpropd  16138  ciclcl  16231  cicrcl  16232  isssc  16249  evlfcl  16631  uncfcurf  16648  pltval  16729  lublecllem  16757  tosso  16805  oduleg  16901  oduclatb  16913  posglbmo  16916  isipodrs  16930  odudlatb  16965  gsumvalx  17039  sgrp2rid2  17182  grplmulf1o  17258  grplactcnv  17287  elnmz  17402  eqgid  17415  isghm  17429  ghmeqker  17456  resscntz  17533  symg1bas  17585  pgrpsubgsymgbi  17596  symgfixelq  17622  f1omvdconj  17635  odmulgeq  17743  sylow3lem3  17813  sylow3lem6  17816  efgval2  17906  efgsdm  17912  efgrelexlema  17931  efgcpbllemb  17937  iscyggen2  18052  cyggenod  18055  gsummptfzcl  18137  eldprd  18172  dprdf11  18191  dprddisj2  18207  pgpfac1lem2  18243  pgpfac1  18248  srg1zr  18298  drngid2  18532  issubrg  18549  islmod  18636  aspval2  19114  psrbag  19131  cply1coe0bi  19437  zndvds  19662  znleval  19667  iunocv  19786  pjfval2  19814  pjdm2  19816  dsmmelbas  19844  ellspd  19902  islindf  19912  islindf4  19938  istopg  20467  basgen2  20546  isclo  20643  mretopd  20648  isnei  20659  isperf3  20709  restdis  20734  neitr  20736  restcls  20737  restlp  20739  restperf  20740  iscn  20791  iscnp  20793  lmbr2  20815  lmbrf  20816  ordtt1  20935  cmpsub  20955  hauscmplem  20961  cmpfi  20963  dfcon2  20974  1stcelcls  21016  1stccn  21018  nllyi  21030  subislly  21036  dissnlocfin  21084  elkgen  21091  ptpjpre1  21126  ptuni2  21131  ptclsg  21170  ptcnplem  21176  txcn  21181  hausdiag  21200  txhaus  21202  txkgen  21207  xkoptsub  21209  cnmpt21  21226  elqtop  21252  tgqtop  21267  r0cld  21293  elfg  21427  fbasrn  21440  trfil2  21443  trfil3  21444  fin1aufil  21488  elfm2  21504  elfm3  21506  flimopn  21531  fbflim  21532  flfnei  21547  flftg  21552  cnpflf2  21556  txflf  21562  fclsbas  21577  alexsubALTlem4  21606  cnextfvval  21621  snclseqg  21671  tgphaus  21672  tsmsfbas  21683  tsmssubm  21698  utopsnneip  21804  prdsxmetlem  21924  imasdsf1olem  21929  xpsdsval  21937  blres  21987  isxms2  22004  metcnp  22097  txmetcnp  22103  txmetcn  22104  metustel  22106  metuel2  22121  dscopn  22129  isngp4  22166  cnblcld  22320  metnrmlem1a  22400  icoopnst  22477  iocopnst  22478  elpi1  22584  isclmp  22636  isncvsngp  22683  lmmbr2  22783  cfil3i  22793  caucfil  22807  iscmet3  22817  lmclim  22826  metcld2  22830  bcthlem4  22849  minveclem3b  22924  minveclem6  22930  minveclem7  22931  ivthle  22949  ivthle2  22950  evthicc2  22953  ovolfioo  22960  ovolficc  22961  ovolgelb  22972  dyadmax  23089  subopnmbl  23095  ismbf3d  23144  mbfimaopnlem  23145  mbfimaopn2  23147  mbfaddlem  23150  mbfsup  23154  mbfinf  23155  i1f1lem  23179  i1fmulclem  23192  itg1climres  23204  mbfi1fseqlem4  23208  itg2monolem1  23240  itg2gt0  23250  isibl  23255  iblcnlem1  23277  ellimc2  23364  dvcnvrelem1  23501  itgsubst  23533  mdegleb  23545  fta1glem2  23647  quotval  23768  vieta1lem1  23786  vieta1lem2  23787  ulm2  23860  ulmcaulem  23869  ulmcau  23870  radcnvlt1  23893  sineq0  23994  cos11  24000  recosf1o  24002  efopn  24121  cxpeq  24215  mcubic  24291  birthdaylem3  24397  rlimcnp  24409  xrlimcnp  24412  eldmgm  24465  dmgmaddn0  24466  lgamgulmlem6  24477  wilth  24514  isppw  24557  isppw2  24558  mumullem2  24623  sqff1o  24625  dvdsmulf1o  24637  fsumvma  24655  fsumvma2  24656  vmasum  24658  chpchtsum  24661  lgsne0  24777  gausslemma2dlem0i  24806  gausslemma2dlem1a  24807  lgseisenlem2  24818  lgsquadlem1  24822  lgsquadlem2  24823  2lgslem1a  24833  dchrmusumlema  24899  rpvmasum2  24918  dchrisum0lema  24920  pntibndlem3  24998  pntlemi  25010  pntleml  25017  pnt3  25018  trgcgrg  25128  tgcgr4  25144  colcom  25171  colrot1  25172  ltgov  25210  hlcomb  25216  lncom  25235  mirreu3  25267  isperp  25325  perpcom  25326  brbtwn  25497  brcgr  25498  brbtwn2  25503  colinearalg  25508  axeuclidlem  25560  axcontlem2  25563  axcontlem4  25565  axcontlem7  25568  nbgraf1olem1  25736  nbgraf1olem5  25740  nbcusgra  25758  uvtx01vtx  25786  cusgrauvtxb  25790  iswlk  25814  istrl  25833  ispth  25864  isspth  25865  wlkdvspthlem  25903  usgrcyclnl2  25935  wwlkn0s  25999  wwlkextwrd  26022  wwlkextproplem3  26037  isclwlk0  26048  clwwlkn2  26069  eclclwwlkn1  26125  eleclclwwlkn  26126  hashecclwwlkn1  26127  usghashecclwwlk  26128  clwlkfclwwlk1hashn  26134  clwlkfoclwwlk  26138  usg2spthonot  26181  isrgra  26219  isrusgra  26220  isrusgusrg  26225  eupath2  26273  frgra3vlem2  26294  frgrancvvdeqlem2  26324  frgrancvvdeqlem3  26325  frgrancvvdeqlemC  26332  usg2spot2nb  26358  isvclem  26598  isnvlem  26633  isphg  26862  isph  26867  phoeqi  26903  ubthlem3  26918  minvecolem5  26927  minvecolem6  26928  minvecolem7  26929  hhph  27225  issh3  27266  nmopub  27957  nmfnleub  27974  adjeq  27984  adjvalval  27986  elunop2  28062  lnophm  28068  nmcexi  28075  cnlnadjlem5  28120  cnlnadjeui  28126  adjbd1o  28134  jpi  28319  mddmd2  28358  chrelati  28413  chrelat2i  28414  cvexchlem  28417  dmdbr5ati  28471  cdjreui  28481  cdj3i  28490  iunxsngf  28564  disjunsn  28595  opeldifid  28600  fcoinvbr  28605  brabgaf  28606  opabdm  28609  opabrn  28610  iunsnima  28614  abfmpunirn  28638  fmptcof2  28645  funcnvmptOLD  28656  funcnvmpt  28657  funcnv5mpt  28658  f1od2  28693  resf1o  28699  fpwrelmap  28702  iocinioc2  28737  eliccioo  28776  posrasymb  28794  isslmd  28892  smatrcl  28996  pstmxmet  29074  prsdm  29094  prsrn  29095  ordtconlem1  29104  xrmulc1cn  29110  ispisys2  29349  elcarsg  29500  eulerpartlemmf  29570  isrrvv  29638  bnj976  29908  bnj944  30068  bnj1173  30130  bnj1321  30155  bnj1373  30158  bnj1417  30169  subfacp1lem3  30224  subfacp1lem6  30227  subfacp1  30228  txpcon  30274  sconpi1  30281  rescon  30288  cvmscbv  30300  cvmsval  30308  cvmlift2lem13  30357  cvmlift3lem2  30362  cvmlift3  30370  mclsrcl  30518  br8  30705  br6  30706  br4  30707  fv1stcnv  30731  fv2ndcnv  30732  distel  30759  poseq  30800  wsuclem  30823  wsuclemOLD  30824  sltsolem1  30873  imageval  31013  funpartfv  31028  dfrdg4  31034  altopthg  31050  altopthbg  31051  brcolinear2  31141  lineext  31159  brsegle  31191  seglelin  31199  broutsideof2  31205  isfne4  31311  isfne2  31313  isfne3  31314  fneval  31323  topfneec  31326  neibastop2lem  31331  neibastop2  31332  neifg  31342  filnetlem4  31352  onsuct0  31416  bj-abbi  31769  bj-tagcg  31962  bj-projval  31973  bj-restuni  32027  csbwrecsg  32145  csboprabg  32148  csbmpt22g  32149  topdifinffinlem  32167  isbasisrelowllem1  32175  isbasisrelowllem2  32176  rdgeqoa  32190  csbfinxpg  32197  wl-sbrimt  32306  wl-sblimt  32307  wl-sbnf1  32311  wl-mo2df  32327  wl-eudf  32329  wl-mo2t  32332  wl-mo3t  32333  wl-ax11-lem6  32342  uncov  32356  tan2h  32367  matunitlindf  32373  ptrest  32374  poimirlem2  32377  poimirlem16  32391  poimirlem19  32394  poimirlem23  32398  poimirlem24  32399  poimirlem25  32400  poimirlem26  32401  poimirlem27  32402  mbfposadd  32423  cnambfre  32424  itg2addnclem2  32428  fdc  32507  heibor1  32575  rrncmslem  32597  rrnheibor  32602  opidonOLD  32617  issmgrpOLD  32628  ismndo  32637  isrngo  32662  isdivrngo  32715  isfldidl2  32834  isdmn3  32839  prtlem13  32967  prter3  32981  lrelat  33115  islshpat  33118  lshpsmreu  33210  lkrpssN  33264  cmtvalN  33312  omllaw2N  33345  cvrval  33370  cvrval2  33375  cvlsupr3  33445  3dim0  33557  islln2  33611  islpln5  33635  islpln2  33636  islpln2ah  33649  islvol5  33679  islvol2  33680  4atlem11  33709  pmapglbx  33869  cdleme18d  34396  cdlemefrs29bpre0  34498  cdlemb3  34708  cdlemg33b  34809  cdlemkid3N  35035  cdlemkid4  35036  dvhb1dimN  35088  dia11N  35151  cdlemm10N  35221  dib11N  35263  dib1dim  35268  dibglbN  35269  diblsmopel  35274  dihopelvalcpre  35351  dih11  35368  dihmeetlem4preN  35409  dihmeetlem13N  35422  lcfrvalsnN  35644  lcfrlem9  35653  lcf1o  35654  mapdval4N  35735  baerlem3lem2  35813  baerlem5alem2  35814  baerlem5blem2  35815  hdmap1fval  35900  hdmapfval  35933  hdmapglem7a  36033  hlhillcs  36064  ellz1  36144  lzunuz  36145  fz1eqin  36146  diophrex  36153  rexrabdioph  36172  rexfrabdioph  36173  2rexfrabdioph  36174  3rexfrabdioph  36175  4rexfrabdioph  36176  6rexfrabdioph  36177  7rexfrabdioph  36178  fzneg  36363  expdioph  36404  wepwsolem  36426  fnwe2lem2  36435  islmodfg  36453  kercvrlsm  36467  sdrgacs  36586  cnvcnvintabd  36721  iunrelexpuztr  36826  brtrclfv2  36834  frege124d  36868  rcompleq  37134  or3or  37135  uneqsn  37137  clsk1independent  37160  ntrclsneine0lem  37178  ntrclsiso  37181  ntrclsk2  37182  ntrclskb  37183  ntrclsk3  37184  ntrclsk13  37185  ntrclsk4  37186  ntrneiel2  37200  ntrneiiso  37205  ntrneikb  37208  ntrneik3  37210  ntrneix3  37211  ntrneik13  37212  ntrneix13  37213  ntrneik4w  37214  k0004lem3  37263  pm10.52  37382  iotasbc  37438  pm14.122a  37441  pm14.122b  37442  pm14.123a  37444  rusbcALT  37458  fvsb  37473  trsbc  37567  rexsngf  38041  iunxsngf2  38051  mapsnd  38179  limcperiod  38492  limsupre  38505  dvbdfbdioo  38617  stoweidlem34  38724  fourierdlem108  38904  fourierdlem110  38906  etransc  38973  2reu4a  39635  funressnfv  39654  dfafn5a  39687  el1fzopredsuc  39746  iccelpart  39769  lighneallem2  39859  dfeven2  39898  gboge7  39983  bgoldbwt  39997  riotaeqimp  40158  elfz2z  40172  isuhgr  40277  isushgr  40278  isupgr  40305  isumgr  40315  isuspgr  40377  isusgr  40378  uhgr0v0e  40459  isfusgrf1  40534  opfusgr  40537  usgr1v0e  40540  nbuhgr2vtx1edgb  40569  edgnbusgreu  40590  nbusgredgeu0  40591  isuvtxa  40616  cusgruvtxb  40639  cplgr3v  40652  cusgrsizeinds  40663  vtxdg0v  40683  vtxd0nedgb  40698  vtxduhgr0nedg  40702  vtxdusgr0edgnelALT  40706  is1wlk  40808  isWlk  40809  1wlk1walk  40838  upgr2wlk  40871  usgr2pthlem  40964  isclWlke  40979  isclWlkupgr  40980  iswwlksnx  41037  wwlksnextwrd  41098  wwlksnextproplem3  41112  umgr2wlk  41151  elwwlks2  41165  elwspths2spth  41166  clwlkclwwlk  41206  clwwlksn2  41212  eclclwwlksn1  41254  eleclclwwlksn  41255  hashecclwwlksn1  41256  umgrhashecclwwlk  41257  clwlksfclwwlk1hashn  41261  clwlksfoclwwlk  41265  clwwlksnun  41276  1pthon2v-av  41315  uhgr3cyclex  41344  isconngr  41351  isconngr1  41352  eupth2lems  41401  isfrgr  41425  frgr0v  41428  frgr3vlem2  41439  frgrncvvdeqlem2  41465  frgrncvvdeqlem3  41466  frgrncvvdeqlemC  41473  fusgr2wsp2nb  41493  ismhm0  41590  inclfusubc  41652  isrnghm  41677  rnghmval2  41680  uzlidlring  41714  lidldomnnring  41715  zrninitoringc  41858  opeliun2xp  41899  snlindsntor  42049  elbigo2  42139  gte-lte  42220  gt-lt  42221
  Copyright terms: Public domain W3C validator