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

Theorem syl6ibr 243
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 219 . 2 (𝜒𝜃)
41, 3syl6 35 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197
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 198
This theorem is referenced by:  3imtr4g  287  nic-ax  1753  nfimdOLD  2402  dfmo  2651  euim  2698  mopick2  2715  2moswap  2722  2eu6  2733  necon3d  3010  necon1d  3011  ralrimd  3158  spcimegf  3491  spcegf  3493  spcimedv  3496  spc2gv  3500  spc3gv  3502  rspcimedv  3515  pwpw0  4545  sssn  4558  pwsnALT  4634  ssiun  4765  ssiun2  4766  wefrc  5318  ssrel  5423  dmcosseq  5602  relssres  5655  trin2  5744  ssrnres  5797  sossfld  5805  wfisg  5942  tron  5973  ordtri3or  5982  oneqmini  6002  fnun  6218  f1oun  6382  brprcneu  6410  ssimaex  6494  chfnrn  6560  dffo4  6607  dffo5  6608  tpres  6701  fvclss  6734  isomin  6821  isofrlem  6824  isoselem  6825  fnoprabg  7001  nnsuc  7322  f1oweALT  7392  bropopvvv  7499  bropfvvvvlem  7500  frxp  7531  poxp  7533  fnse  7538  mpt2xopynvov0g  7585  issmo2  7692  smores  7695  smogt  7710  rdglim2  7774  tz7.48lem  7782  tz7.49  7786  swoer  8019  qsss  8053  domtriord  8355  pssnn  8427  ssfi  8429  findcard  8448  findcard2  8449  findcard3  8452  frfi  8454  dffi3  8586  supmo  8607  infmo  8650  inf3lem4  8785  carddom2  9096  fidomtri2  9113  pm54.43  9119  infpwfien  9178  alephordi  9190  cardaleph  9205  carduniima  9212  cardinfima  9213  alephval3  9226  dfac5lem4  9242  dfac5  9244  dfac2b  9246  dfac2OLD  9248  kmlem2  9268  cflm  9367  cfslb2n  9385  cfsmolem  9387  isf32lem9  9478  axcc4  9556  domtriomlem  9559  zorn2lem4  9616  zorn2lem6  9618  fpwwe2lem11  9757  fpwwe2lem12  9758  inttsk  9891  inar1  9892  intgru  9931  ingru  9932  indpi  10024  nqpr  10131  ltaddpr  10151  ltexprlem1  10153  ltexprlem5  10157  reclem2pr  10165  reclem4pr  10167  negn0  10754  zmulcl  11712  uzm1  11956  uzwo  11990  xmullem2  12333  icoshft  12535  difreicc  12547  fzouzsplit  12747  ssfzoulel  12806  seqf1olem1  13083  seqf1olem2  13084  hashge2el2difr  13500  hashtpg  13504  swrdccatin2  13731  modfsummod  14768  incexclem  14810  sqrt2irr  15219  dvds2lem  15237  dvdslelem  15274  oddnn02np1  15312  divalglem8  15363  dfgcd2  15502  euclemma  15662  iserodd  15777  ramcl  15970  setsstruct  16129  mreiincl  16481  joinfval  17226  meetfval  17240  dirge  17462  sylow2alem1  18253  efgredlemb  18380  kerf1hrm  18967  rmodislmodlem  19154  lbspss  19309  lspsneu  19350  lspsnat  19373  lspsncv0  19374  lspsncv0OLD  19375  opsrtoslem2  19713  distop  21034  epttop  21048  isclo2  21127  restdis  21217  subbascn  21293  cnrest2  21325  cnpresti  21327  isnrm2  21397  cmpsublem  21437  cmpcld  21440  dfconn2  21457  t1connperf  21474  1stcrest  21491  lly1stc  21534  uptx  21663  txcn  21664  prdstopn  21666  txconn  21727  cmphaushmeo  21838  fbasrn  21922  csdfil  21932  trufil  21948  fclscf  22063  alexsubALTlem3  22087  alexsubALT  22089  haustsms2  22174  ovoliunlem1  23506  ovoliunnul  23511  volsup2  23609  coeaddlem  24242  plymul0or  24273  radcnv0  24407  wilthlem3  25033  chtub  25174  gausslemma2dlem1a  25327  2sqlem10  25390  pntpbnd1  25512  mptelee  26012  axeuclidlem  26079  axcontlem4  26084  uhgrissubgr  26406  nbgrnself2OLD  26498  finsumvtxdg2size  26697  wlkonl1iedg  26812  pthdivtx  26876  wlkiswwlksupgr2  27027  eucrct2eupth  27441  isch3  28449  shmodsi  28599  orthin  28656  h1datomi  28791  stcltr2i  29485  atom1d  29563  sumdmdii  29625  cdj3lem1  29644  disjpreima  29745  lmxrge0  30346  dmvlsiga  30540  sibfof  30750  bnj600  31334  bnj1018  31377  bnj1173  31415  bnj1174  31416  erdszelem9  31526  cvmlift2lem1  31629  fundmpss  32008  tfisg  32058  frpoinsg  32084  frinsg  32088  poseq  32096  sltval2  32152  outsideofrflx  32577  nn0prpwlem  32660  ivthALT  32673  fnessref  32695  neibastop2lem  32698  tailfb  32715  bj-axtd  32915  bj-nfimt  32954  bj-ssbequ1  32981  bj-nfdt0  33022  bj-2upleq  33329  bj-restn0  33373  icorempt2  33534  isbasisrelowllem2  33539  wl-ax8clv2  33713  matunitlindflem1  33737  poimirlem3  33744  poimirlem4  33745  poimirlem29  33770  mblfinlem3  33780  itg2addnclem3  33794  cover2  33839  fdc  33871  nninfnub  33877  equivtotbnd  33907  prdstotbnd  33923  cntotbnd  33925  ablo4pnp  34009  isdrngo3  34088  crngohomfo  34135  intidl  34158  or32dd  34226  iss2  34444  prtlem18  34675  prter2  34679  lsat0cv  34832  lfl1  34869  lkreqN  34969  atlrelat1  35120  pmaple  35560  pmapsub  35567  pclclN  35690  pclfinN  35699  osumcllem4N  35758  pexmidlem1N  35769  cdleme7ga  36047  lcfl7N  37300  ss2iundf  38469  brtrclfv2  38537  nzss  39034  3impexpbicom  39201  alrim3con13v  39259  tratrb  39262  onfrALTlem3  39275  onfrALTlem2  39277  onfrALTlem1  39279  trsspwALT2  39561  trsspwALT3  39562  2reu1  41716  afv2orxorb  41835  lswn0  41973  lighneallem4b  42119  sbgoldbwt  42258  sbgoldbst  42259  sbgoldbalt  42262  isupwlkg  42304  2zrngamgm  42525  fldivexpfllog2  42945
  Copyright terms: Public domain W3C validator