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

Theorem syl6ibr 253
Description: A mixed syllogism inference from a nested implication and a biconditional. Useful for substituting an embedded consequent with a definition. (Contributed by NM, 10-Jan-1993.)
Hypotheses
Ref Expression
syl6ibr.1 (𝜑 → (𝜓𝜒))
syl6ibr.2 (𝜃𝜒)
Assertion
Ref Expression
syl6ibr (𝜑 → (𝜓𝜃))

Proof of Theorem syl6ibr
StepHypRef Expression
1 syl6ibr.1 . 2 (𝜑 → (𝜓𝜒))
2 syl6ibr.2 . . 3 (𝜃𝜒)
32biimpri 229 . 2 (𝜒𝜃)
41, 3syl6 35 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207
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 208
This theorem is referenced by:  3imtr4g  297  nic-ax  1665  sbequ1  2240  dfmoeu  2614  euimOLD  2698  2moswapv  2710  mopick2  2718  2moswap  2725  2eu6  2740  necon3d  3037  necon1d  3038  ralrimd  3218  spcimegf  3589  spcegf  3591  spcimedv  3594  spc2gv  3600  spc3gv  3604  rspcimedv  3613  2reu1  3880  pwpw0  4740  sssn  4753  pwsnALT  4825  ssiun  4962  ssiun2  4963  wefrc  5543  ssrel  5651  dmcosseq  5838  relssres  5887  trin2  5977  ssrnres  6029  sossfld  6037  reuop  6138  wfisg  6177  tron  6208  ordtri3or  6217  oneqmini  6236  fnun  6457  f1oun  6628  brprcneu  6656  ssimaex  6742  chfnrn  6812  dffo4  6862  dffo5  6863  tpres  6956  fvclss  6992  isomin  7079  isofrlem  7082  isoselem  7083  fnoprabg  7264  nnsuc  7585  f1oweALT  7664  releldmdifi  7735  bropopvvv  7776  bropfvvvvlem  7777  frxp  7811  poxp  7813  fnse  7818  mpoxopynvov0g  7871  issmo2  7977  smores  7980  smogt  7995  rdglim2  8059  tz7.48lem  8068  tz7.49  8072  swoer  8309  qsss  8348  domtriord  8652  pssnn  8725  ssfi  8727  findcard  8746  findcard2  8747  findcard3  8750  frfi  8752  dffi3  8884  supmo  8905  infmo  8948  inf3lem4  9083  carddom2  9395  fidomtri2  9412  pm54.43  9418  infpwfien  9477  alephordi  9489  cardaleph  9504  carduniima  9511  cardinfima  9512  alephval3  9525  dfac5lem4  9541  dfac5  9543  dfac2b  9545  kmlem2  9566  cflm  9661  cfslb2n  9679  cfsmolem  9681  isf32lem9  9772  axcc4  9850  domtriomlem  9853  zorn2lem4  9910  zorn2lem6  9912  fpwwe2lem11  10051  fpwwe2lem12  10052  inttsk  10185  inar1  10186  intgru  10225  ingru  10226  indpi  10318  nqpr  10425  ltaddpr  10445  ltexprlem1  10447  ltexprlem5  10451  reclem2pr  10459  reclem4pr  10461  negn0  11058  zmulcl  12020  uzm1  12265  uzwo  12300  xmullem2  12648  icoshft  12849  difreicc  12860  fzouzsplit  13062  ssfzoulel  13121  seqf1olem1  13399  seqf1olem2  13400  hashge2el2difr  13829  hashtpg  13833  reusq0  14812  modfsummod  15139  incexclem  15181  sqrt2irr  15592  dvds2lem  15612  dvdslelem  15649  oddnn02np1  15687  divalglem8  15741  dfgcd2  15884  2mulprm  16027  ge2nprmge4  16035  euclemma  16047  iserodd  16162  ramcl  16355  setsstruct  16513  mreiincl  16857  joinfval  17601  meetfval  17615  dirge  17837  sylow2alem1  18673  efgredlemb  18803  kerf1ghm  19428  kerf1hrmOLD  19429  rmodislmodlem  19632  lbspss  19785  lspsneu  19826  lspsnat  19848  lspsncv0  19849  opsrtoslem2  20195  distop  21533  epttop  21547  isclo2  21626  restdis  21716  subbascn  21792  cnrest2  21824  cnpresti  21826  isnrm2  21896  cmpsublem  21937  cmpcld  21940  dfconn2  21957  t1connperf  21974  1stcrest  21991  lly1stc  22034  uptx  22163  txcn  22164  prdstopn  22166  txconn  22227  cmphaushmeo  22338  fbasrn  22422  csdfil  22432  trufil  22448  fclscf  22563  alexsubALTlem3  22587  alexsubALT  22589  haustsms2  22674  ovoliunlem1  24032  ovoliunnul  24037  volsup2  24135  coeaddlem  24768  plymul0or  24799  radcnv0  24933  wilthlem3  25575  chtub  25716  gausslemma2dlem1a  25869  2sqlem10  25932  pntpbnd1  26090  mptelee  26609  axeuclidlem  26676  axcontlem4  26681  elntg2  26699  uhgrissubgr  26985  finsumvtxdg2size  27260  wlkonl1iedg  27375  pthdivtx  27438  wlkiswwlksupgr2  27583  eucrct2eupth  27952  isch3  28946  shmodsi  29094  orthin  29151  h1datomi  29286  stcltr2i  29980  atom1d  30058  sumdmdii  30120  cdj3lem1  30139  disjpreima  30263  lmxrge0  31095  dmvlsiga  31288  sibfof  31498  bnj600  32091  bnj1018  32134  bnj1173  32172  bnj1174  32173  pthisspthorcycl  32273  subgrwlk  32277  cusgracyclt3v  32301  erdszelem9  32344  cvmlift2lem1  32447  satfvsucsuc  32510  sat1el2xp  32524  fmla0xp  32528  fundmpss  32907  tfisg  32953  frpoinsg  32979  frinsg  32985  poseq  32993  sltval2  33061  outsideofrflx  33486  nn0prpwlem  33568  ivthALT  33581  fnessref  33603  neibastop2lem  33606  tailfb  33623  bj-axtd  33826  bj-nfimt  33869  bj-nfdt0  33927  bj-nnfand  33976  bj-sbievw2  34068  bj-2upleq  34222  bj-restn0  34276  icorempo  34515  isbasisrelowllem2  34520  rdgellim  34540  rdgssun  34542  pibt2  34581  wl-lem-moexsb  34686  matunitlindflem1  34770  poimirlem3  34777  poimirlem4  34778  poimirlem29  34803  mblfinlem3  34813  itg2addnclem3  34827  cover2  34872  fdc  34903  nninfnub  34909  equivtotbnd  34939  prdstotbnd  34955  cntotbnd  34957  ablo4pnp  35041  isdrngo3  35120  crngohomfo  35167  intidl  35190  or32dd  35255  iss2  35484  prtlem18  35895  prter2  35899  lsat0cv  36051  lfl1  36088  lkreqN  36188  atlrelat1  36339  pmaple  36779  pmapsub  36786  pclclN  36909  pclfinN  36918  osumcllem4N  36977  pexmidlem1N  36988  cdleme7ga  37266  lcfl7N  38519  rtprmirr  39074  ss2iundf  39884  brtrclfv2  39952  nzss  40529  3impexpbicom  40693  alrim3con13v  40747  tratrb  40750  onfrALTlem3  40758  onfrALTlem2  40760  onfrALTlem1  40762  trsspwALT2  41033  trsspwALT3  41034  or2expropbi  43150  afv2orxorb  43308  lswn0  43451  ich2exprop  43480  prproropf1olem4  43515  paireqne  43520  reupr  43531  lighneallem4b  43621  sbgoldbwt  43789  sbgoldbst  43790  sbgoldbalt  43793  isomuspgrlem1  43839  isomuspgrlem2d  43843  isupwlkg  43859  2zrngamgm  44108  fldivexpfllog2  44523  line2ylem  44636
  Copyright terms: Public domain W3C validator