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

Theorem syl6ibr 242
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 218 . 2 (𝜒𝜃)
41, 3syl6 35 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:  3imtr4g  285  imp4aOLD  614  nic-ax  1638  nfimt  1861  nfimdOLD  2262  mo2v  2505  euim  2552  mopick2  2569  2moswap  2576  2eu6  2587  necon3d  2844  necon1d  2845  ralrimd  2988  spcimegf  3318  spcegf  3320  spcimedv  3323  spc2gv  3327  spc3gv  3329  rspcimedv  3342  eqsbc3rOLD  3526  pwpw0  4376  sssn  4390  pwsnALT  4461  ssiun  4594  ssiun2  4595  wefrc  5137  ssrel  5241  dmcosseq  5419  relssres  5472  restidsingOLD  5494  trin2  5554  ssrnres  5607  sossfld  5615  wfisg  5753  tron  5784  ordtri3or  5793  oneqmini  5814  fnun  6035  f1oun  6194  brprcneu  6222  ssimaex  6302  chfnrn  6368  dffo4  6415  dffo5  6416  tpres  6507  fvclss  6540  isomin  6627  isofrlem  6630  isoselem  6631  fnoprabg  6803  nnsuc  7124  f1oweALT  7194  bropopvvv  7300  bropfvvvvlem  7301  frxp  7332  poxp  7334  fnse  7339  mpt2xopynvov0g  7385  issmo2  7491  smores  7494  smogt  7509  rdglim2  7573  tz7.48lem  7581  tz7.49  7585  swoer  7817  qsss  7851  domtriord  8147  pssnn  8219  ssfi  8221  findcard  8240  findcard2  8241  findcard3  8244  frfi  8246  dffi3  8378  supmo  8399  infmo  8442  inf3lem4  8566  carddom2  8841  fidomtri2  8858  pm54.43  8864  infpwfien  8923  alephordi  8935  cardaleph  8950  carduniima  8957  cardinfima  8958  alephval3  8971  dfac5lem4  8987  dfac5  8989  dfac2  8991  kmlem2  9011  cflm  9110  cfslb2n  9128  cfsmolem  9130  isf32lem9  9221  axcc4  9299  domtriomlem  9302  zorn2lem4  9359  zorn2lem6  9361  fpwwe2lem11  9500  fpwwe2lem12  9501  inttsk  9634  inar1  9635  intgru  9674  ingru  9675  indpi  9767  nqpr  9874  ltaddpr  9894  ltexprlem1  9896  ltexprlem5  9900  reclem2pr  9908  reclem4pr  9910  negn0  10497  zmulcl  11464  uzm1  11756  uzwo  11789  xmullem2  12133  icoshft  12332  difreicc  12342  fzouzsplit  12542  ssfzoulel  12602  seqf1olem1  12880  seqf1olem2  12881  hashge2el2difr  13301  hashtpg  13305  swrdccatin2  13533  modfsummod  14570  incexclem  14612  sqrt2irr  15023  dvds2lem  15041  dvdslelem  15078  oddnn02np1  15119  divalglem8  15170  dfgcd2  15310  euclemma  15472  iserodd  15587  ramcl  15780  setsstruct  15945  mreiincl  16303  joinfval  17048  meetfval  17062  dirge  17284  sylow2alem1  18078  efgredlemb  18205  kerf1hrm  18791  rmodislmodlem  18978  lbspss  19130  lspsneu  19171  lspsnat  19193  lspsncv0  19194  opsrtoslem2  19533  distop  20847  epttop  20861  isclo2  20940  restdis  21030  subbascn  21106  cnrest2  21138  cnpresti  21140  isnrm2  21210  cmpsublem  21250  cmpcld  21253  dfconn2  21270  t1connperf  21287  1stcrest  21304  lly1stc  21347  uptx  21476  txcn  21477  prdstopn  21479  txconn  21540  cmphaushmeo  21651  fbasrn  21735  csdfil  21745  trufil  21761  fclscf  21876  alexsubALTlem3  21900  alexsubALT  21902  haustsms2  21987  ovoliunlem1  23316  ovoliunnul  23321  volsup2  23419  coeaddlem  24050  plymul0or  24081  radcnv0  24215  wilthlem3  24841  chtub  24982  gausslemma2dlem1a  25135  2sqlem10  25198  pntpbnd1  25320  mptelee  25820  axeuclidlem  25887  axcontlem4  25892  uhgrissubgr  26212  nbgrnself2OLD  26304  finsumvtxdg2size  26502  wlkonl1iedg  26617  pthdivtx  26681  wlkiswwlksupgr2  26831  eucrct2eupth  27223  isch3  28226  shmodsi  28376  orthin  28433  h1datomi  28568  stcltr2i  29262  atom1d  29340  sumdmdii  29402  cdj3lem1  29421  disjpreima  29523  lmxrge0  30126  dmvlsiga  30320  sibfof  30530  bnj600  31115  bnj1018  31158  bnj1173  31196  bnj1174  31197  erdszelem9  31307  cvmlift2lem1  31410  fundmpss  31790  tfisg  31840  frpoinsg  31866  frinsg  31870  poseq  31878  sltval2  31934  outsideofrflx  32359  nn0prpwlem  32442  ivthALT  32455  fnessref  32477  neibastop2lem  32480  tailfb  32497  bj-axtd  32703  bj-ssbequ1  32769  bj-nfdt0  32810  bj-2upleq  33125  bj-restn0  33168  icorempt2  33329  isbasisrelowllem2  33334  wl-ax8clv2  33511  matunitlindflem1  33535  poimirlem3  33542  poimirlem4  33543  poimirlem29  33568  mblfinlem3  33578  itg2addnclem3  33593  cover2  33638  fdc  33671  nninfnub  33677  equivtotbnd  33707  prdstotbnd  33723  cntotbnd  33725  ablo4pnp  33809  isdrngo3  33888  crngohomfo  33935  intidl  33958  or32dd  34026  iss2  34252  prtlem18  34481  prter2  34485  lsat0cv  34638  lfl1  34675  lkreqN  34775  atlrelat1  34926  pmaple  35365  pmapsub  35372  pclclN  35495  pclfinN  35504  osumcllem4N  35563  pexmidlem1N  35574  cdleme7ga  35853  lcfl7N  37107  ss2iundf  38268  brtrclfv2  38336  nzss  38833  3impexpbicom  39002  alrim3con13v  39060  tratrb  39063  onfrALTlem3  39076  onfrALTlem2  39078  onfrALTlem1  39080  trsspwALT2  39363  trsspwALT3  39364  2reu1  41507  lswn0  41705  lighneallem4b  41851  sbgoldbwt  41990  sbgoldbst  41991  sbgoldbalt  41994  isupwlkg  42043  2zrngamgm  42264  fldivexpfllog2  42684
  Copyright terms: Public domain W3C validator