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

Theorem syl6ibr 255
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 231 . 2 (𝜒𝜃)
41, 3syl6 35 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209
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 210
This theorem is referenced by:  3imtr4g  299  nic-ax  1675  sbequ1  2248  dfmoeu  2597  euimOLD  2682  2moswapv  2694  mopick2  2702  2moswap  2709  2eu6  2722  necon3d  3011  necon1d  3012  ralrimd  3185  spcimegf  3540  spcegf  3542  spcimedv  3545  spc2gv  3552  spc3gv  3556  rspcimedv  3565  2reu1  3829  pwpw0  4709  sssn  4722  pwsnOLD  4796  ssiun  4936  ssiun2  4937  wefrc  5517  ssrel  5625  dmcosseq  5813  relssres  5863  trin2  5954  ssrnres  6006  sossfld  6014  reuop  6116  wfisg  6155  tron  6186  ordtri3or  6195  oneqmini  6214  fnun  6438  f1oun  6613  brprcneu  6641  ssimaex  6727  chfnrn  6800  dffo4  6850  dffo5  6851  tpres  6944  fvclss  6983  isomin  7073  isofrlem  7076  isoselem  7077  fnoprabg  7258  nnsuc  7581  f1oweALT  7659  releldmdifi  7730  bropopvvv  7772  bropfvvvvlem  7773  frxp  7807  poxp  7809  fnse  7814  mpoxopynvov0g  7867  issmo2  7973  smores  7976  smogt  7991  rdglim2  8055  tz7.48lem  8064  tz7.49  8068  swoer  8306  qsss  8345  domtriord  8651  pssnn  8724  ssfi  8726  findcard  8745  findcard2  8746  findcard3  8749  frfi  8751  dffi3  8883  supmo  8904  infmo  8947  inf3lem4  9082  carddom2  9394  fidomtri2  9411  pm54.43  9418  infpwfien  9477  alephordi  9489  cardaleph  9504  carduniima  9511  cardinfima  9512  alephval3  9525  dfac5lem4  9541  dfac5  9543  dfac2b  9545  kmlem2  9566  cflm  9665  cfslb2n  9683  cfsmolem  9685  isf32lem9  9776  axcc4  9854  domtriomlem  9857  zorn2lem4  9914  zorn2lem6  9916  fpwwe2lem11  10055  fpwwe2lem12  10056  inttsk  10189  inar1  10190  intgru  10229  ingru  10230  indpi  10322  nqpr  10429  ltaddpr  10449  ltexprlem1  10451  ltexprlem5  10455  reclem2pr  10463  reclem4pr  10465  negn0  11062  zmulcl  12023  uzm1  12268  uzwo  12303  xmullem2  12650  icoshft  12855  difreicc  12866  fzouzsplit  13071  ssfzoulel  13130  seqf1olem1  13409  seqf1olem2  13410  hashge2el2difr  13839  hashtpg  13843  reusq0  14817  modfsummod  15144  incexclem  15186  sqrt2irr  15597  dvds2lem  15617  dvdslelem  15654  oddnn02np1  15692  divalglem8  15744  dfgcd2  15887  2mulprm  16030  ge2nprmge4  16038  euclemma  16050  iserodd  16165  ramcl  16358  setsstruct  16518  mreiincl  16862  joinfval  17606  meetfval  17620  dirge  17842  sylow2alem1  18737  efgredlemb  18867  kerf1ghm  19494  rmodislmodlem  19697  lbspss  19850  lspsneu  19891  lspsnat  19913  lspsncv0  19914  opsrtoslem2  20727  mhpvarcl  20801  distop  21603  epttop  21617  isclo2  21696  restdis  21786  subbascn  21862  cnrest2  21894  cnpresti  21896  isnrm2  21966  cmpsublem  22007  cmpcld  22010  dfconn2  22027  t1connperf  22044  1stcrest  22061  lly1stc  22104  uptx  22233  txcn  22234  prdstopn  22236  txconn  22297  cmphaushmeo  22408  fbasrn  22492  csdfil  22502  trufil  22518  fclscf  22633  alexsubALTlem3  22657  alexsubALT  22659  haustsms2  22745  ovoliunlem1  24109  ovoliunnul  24114  volsup2  24212  coeaddlem  24849  plymul0or  24880  radcnv0  25014  wilthlem3  25658  chtub  25799  gausslemma2dlem1a  25952  2sqlem10  26015  pntpbnd1  26173  mptelee  26692  axeuclidlem  26759  axcontlem4  26764  elntg2  26782  uhgrissubgr  27068  finsumvtxdg2size  27343  wlkonl1iedg  27458  pthdivtx  27521  wlkiswwlksupgr2  27666  eucrct2eupth  28033  isch3  29027  shmodsi  29175  orthin  29232  h1datomi  29367  stcltr2i  30061  atom1d  30139  sumdmdii  30201  cdj3lem1  30220  disjpreima  30350  lmxrge0  31303  dmvlsiga  31496  sibfof  31706  bnj600  32299  bnj1018g  32343  bnj1018  32344  bnj1173  32382  bnj1174  32383  pthisspthorcycl  32483  subgrwlk  32487  cusgracyclt3v  32511  erdszelem9  32554  cvmlift2lem1  32657  satfvsucsuc  32720  sat1el2xp  32734  fmla0xp  32738  fundmpss  33117  tfisg  33163  frpoinsg  33189  frinsg  33195  poseq  33203  sltval2  33271  outsideofrflx  33696  nn0prpwlem  33778  ivthALT  33791  fnessref  33813  neibastop2lem  33816  tailfb  33833  bj-axtd  34036  bj-nfimt  34079  bj-nfdt0  34137  bj-nnfand  34188  bj-sbievw2  34280  bj-2upleq  34443  bj-restn0  34500  icorempo  34763  isbasisrelowllem2  34768  rdgellim  34788  rdgssun  34790  pibt2  34829  wl-lem-moexsb  34962  matunitlindflem1  35046  poimirlem3  35053  poimirlem4  35054  poimirlem29  35079  mblfinlem3  35089  itg2addnclem3  35103  cover2  35145  fdc  35176  nninfnub  35182  equivtotbnd  35209  prdstotbnd  35225  cntotbnd  35227  ablo4pnp  35311  isdrngo3  35390  crngohomfo  35437  intidl  35460  or32dd  35525  iss2  35754  prtlem18  36166  prter2  36170  lsat0cv  36322  lfl1  36359  lkreqN  36459  atlrelat1  36610  pmaple  37050  pmapsub  37057  pclclN  37180  pclfinN  37189  osumcllem4N  37248  pexmidlem1N  37259  cdleme7ga  37537  lcfl7N  38790  rtprmirr  39489  ss2iundf  40347  brtrclfv2  40415  nzss  41008  3impexpbicom  41172  alrim3con13v  41226  tratrb  41229  onfrALTlem3  41237  onfrALTlem2  41239  onfrALTlem1  41241  trsspwALT2  41512  trsspwALT3  41513  or2expropbi  43613  afv2orxorb  43771  lswn0  43948  ich2exprop  43975  prproropf1olem4  44010  paireqne  44015  reupr  44026  lighneallem4b  44114  sbgoldbwt  44282  sbgoldbst  44283  sbgoldbalt  44286  isomuspgrlem1  44332  isomuspgrlem2d  44336  isupwlkg  44352  2zrngamgm  44550  fldivexpfllog2  44966  line2ylem  45152
  Copyright terms: Public domain W3C validator