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  616  nic-ax  1735  nfimt  1958  nfimdOLD  2359  mo2v  2602  euim  2649  mopick2  2666  2moswap  2673  2eu6  2684  necon3d  2941  necon1d  2942  ralrimd  3085  spcimegf  3415  spcegf  3417  spcimedv  3420  spc2gv  3424  spc3gv  3426  rspcimedv  3439  eqsbc3rOLD  3622  pwpw0  4477  sssn  4491  pwsnALT  4569  ssiun  4702  ssiun2  4703  wefrc  5248  ssrel  5352  dmcosseq  5530  relssres  5583  restidsingOLD  5605  trin2  5665  ssrnres  5718  sossfld  5726  wfisg  5864  tron  5895  ordtri3or  5904  oneqmini  5925  fnun  6146  f1oun  6305  brprcneu  6333  ssimaex  6413  chfnrn  6479  dffo4  6526  dffo5  6527  tpres  6618  fvclss  6651  isomin  6738  isofrlem  6741  isoselem  6742  fnoprabg  6914  nnsuc  7235  f1oweALT  7305  bropopvvv  7411  bropfvvvvlem  7412  frxp  7443  poxp  7445  fnse  7450  mpt2xopynvov0g  7497  issmo2  7603  smores  7606  smogt  7621  rdglim2  7685  tz7.48lem  7693  tz7.49  7697  swoer  7929  qsss  7963  domtriord  8259  pssnn  8331  ssfi  8333  findcard  8352  findcard2  8353  findcard3  8356  frfi  8358  dffi3  8490  supmo  8511  infmo  8554  inf3lem4  8689  carddom2  8964  fidomtri2  8981  pm54.43  8987  infpwfien  9046  alephordi  9058  cardaleph  9073  carduniima  9080  cardinfima  9081  alephval3  9094  dfac5lem4  9110  dfac5  9112  dfac2b  9114  dfac2OLD  9116  kmlem2  9136  cflm  9235  cfslb2n  9253  cfsmolem  9255  isf32lem9  9346  axcc4  9424  domtriomlem  9427  zorn2lem4  9484  zorn2lem6  9486  fpwwe2lem11  9625  fpwwe2lem12  9626  inttsk  9759  inar1  9760  intgru  9799  ingru  9800  indpi  9892  nqpr  9999  ltaddpr  10019  ltexprlem1  10021  ltexprlem5  10025  reclem2pr  10033  reclem4pr  10035  negn0  10622  zmulcl  11589  uzm1  11882  uzwo  11915  xmullem2  12259  icoshft  12458  difreicc  12468  fzouzsplit  12668  ssfzoulel  12727  seqf1olem1  13005  seqf1olem2  13006  hashge2el2difr  13426  hashtpg  13430  swrdccatin2  13658  modfsummod  14696  incexclem  14738  sqrt2irr  15149  dvds2lem  15167  dvdslelem  15204  oddnn02np1  15245  divalglem8  15296  dfgcd2  15436  euclemma  15598  iserodd  15713  ramcl  15906  setsstruct  16071  mreiincl  16429  joinfval  17173  meetfval  17187  dirge  17409  sylow2alem1  18203  efgredlemb  18330  kerf1hrm  18916  rmodislmodlem  19103  lbspss  19255  lspsneu  19296  lspsnat  19318  lspsncv0  19319  opsrtoslem2  19658  distop  20972  epttop  20986  isclo2  21065  restdis  21155  subbascn  21231  cnrest2  21263  cnpresti  21265  isnrm2  21335  cmpsublem  21375  cmpcld  21378  dfconn2  21395  t1connperf  21412  1stcrest  21429  lly1stc  21472  uptx  21601  txcn  21602  prdstopn  21604  txconn  21665  cmphaushmeo  21776  fbasrn  21860  csdfil  21870  trufil  21886  fclscf  22001  alexsubALTlem3  22025  alexsubALT  22027  haustsms2  22112  ovoliunlem1  23441  ovoliunnul  23446  volsup2  23544  coeaddlem  24175  plymul0or  24206  radcnv0  24340  wilthlem3  24966  chtub  25107  gausslemma2dlem1a  25260  2sqlem10  25323  pntpbnd1  25445  mptelee  25945  axeuclidlem  26012  axcontlem4  26017  uhgrissubgr  26337  nbgrnself2OLD  26429  finsumvtxdg2size  26627  wlkonl1iedg  26742  pthdivtx  26806  wlkiswwlksupgr2  26957  eucrct2eupth  27368  isch3  28378  shmodsi  28528  orthin  28585  h1datomi  28720  stcltr2i  29414  atom1d  29492  sumdmdii  29554  cdj3lem1  29573  disjpreima  29675  lmxrge0  30278  dmvlsiga  30472  sibfof  30682  bnj600  31267  bnj1018  31310  bnj1173  31348  bnj1174  31349  erdszelem9  31459  cvmlift2lem1  31562  fundmpss  31942  tfisg  31992  frpoinsg  32018  frinsg  32022  poseq  32030  sltval2  32086  outsideofrflx  32511  nn0prpwlem  32594  ivthALT  32607  fnessref  32629  neibastop2lem  32632  tailfb  32649  bj-axtd  32855  bj-ssbequ1  32921  bj-nfdt0  32962  bj-2upleq  33277  bj-restn0  33320  icorempt2  33481  isbasisrelowllem2  33486  wl-ax8clv2  33663  matunitlindflem1  33687  poimirlem3  33694  poimirlem4  33695  poimirlem29  33720  mblfinlem3  33730  itg2addnclem3  33745  cover2  33790  fdc  33823  nninfnub  33829  equivtotbnd  33859  prdstotbnd  33875  cntotbnd  33877  ablo4pnp  33961  isdrngo3  34040  crngohomfo  34087  intidl  34110  or32dd  34178  iss2  34404  prtlem18  34635  prter2  34639  lsat0cv  34792  lfl1  34829  lkreqN  34929  atlrelat1  35080  pmaple  35519  pmapsub  35526  pclclN  35649  pclfinN  35658  osumcllem4N  35717  pexmidlem1N  35728  cdleme7ga  36007  lcfl7N  37261  ss2iundf  38422  brtrclfv2  38490  nzss  38987  3impexpbicom  39156  alrim3con13v  39214  tratrb  39217  onfrALTlem3  39230  onfrALTlem2  39232  onfrALTlem1  39234  trsspwALT2  39517  trsspwALT3  39518  2reu1  41661  lswn0  41859  lighneallem4b  42005  sbgoldbwt  42144  sbgoldbst  42145  sbgoldbalt  42148  isupwlkg  42197  2zrngamgm  42418  fldivexpfllog2  42838
  Copyright terms: Public domain W3C validator