Theorem syl6ibr 244

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

Step	Hyp	Ref	Expression
1		syl6ibr.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		syl6ibr.2	. . 3 ⊢ (𝜃 ↔ 𝜒)
3	2	biimpri 220	. 2 ⊢ (𝜒 → 𝜃)
4	1, 3	syl6 35	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 198

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 199

This theorem is referenced by:  3imtr4g  288  nic-ax  1636  sbequ1  2174  dfmolem  2584  euim  2647  2moswapv  2659  mopick2  2665  2moswap  2672  2eu6  2685  necon3d  2985  necon1d  2986  ralrimd  3165  spcimegf  3505  spcegf  3507  spcimedv  3510  spc2gv  3516  spc3gv  3520  rspcimedv  3534  2reu1  3783  pwpw0  4618  sssn  4631  pwsnALT  4703  ssiun  4834  ssiun2  4835  wefrc  5398  ssrel  5504  dmcosseq  5683  relssres  5736  trin2  5821  ssrnres  5873  sossfld  5881  reuop  5980  wfisg  6019  tron  6050  ordtri3or  6059  oneqmini  6078  fnun  6294  f1oun  6461  brprcneu  6489  ssimaex  6574  chfnrn  6642  dffo4  6690  dffo5  6691  tpres  6788  fvclss  6824  isomin  6911  isofrlem  6914  isoselem  6915  fnoprabg  7089  nnsuc  7411  f1oweALT  7482  bropopvvv  7590  bropfvvvvlem  7591  frxp  7622  poxp  7624  fnse  7629  mpoxopynvov0g  7680  issmo2  7787  smores  7790  smogt  7805  rdglim2  7869  tz7.48lem  7877  tz7.49  7881  swoer  8115  qsss  8154  domtriord  8455  pssnn  8527  ssfi  8529  findcard  8548  findcard2  8549  findcard3  8552  frfi  8554  dffi3  8686  supmo  8707  infmo  8750  inf3lem4  8884  carddom2  9196  fidomtri2  9213  pm54.43  9219  infpwfien  9278  alephordi  9290  cardaleph  9305  carduniima  9312  cardinfima  9313  alephval3  9326  dfac5lem4  9342  dfac5  9344  dfac2b  9346  kmlem2  9367  cflm  9466  cfslb2n  9484  cfsmolem  9486  isf32lem9  9577  axcc4  9655  domtriomlem  9658  zorn2lem4  9715  zorn2lem6  9717  fpwwe2lem11  9856  fpwwe2lem12  9857  inttsk  9990  inar1  9991  intgru  10030  ingru  10031  indpi  10123  nqpr  10230  ltaddpr  10250  ltexprlem1  10252  ltexprlem5  10256  reclem2pr  10264  reclem4pr  10266  negn0  10866  zmulcl  11841  uzm1  12087  uzwo  12122  xmullem2  12471  icoshft  12672  difreicc  12683  fzouzsplit  12884  ssfzoulel  12943  seqf1olem1  13221  seqf1olem2  13222  hashge2el2difr  13644  hashtpg  13648  swrdccatin2  13923  reusq0  14677  modfsummod  15003  incexclem  15045  sqrt2irr  15456  dvds2lem  15476  dvdslelem  15513  oddnn02np1  15551  divalglem8  15605  dfgcd2  15744  2mulprm  15887  ge2nprmge4  15895  euclemma  15907  iserodd  16022  ramcl  16215  setsstruct  16373  mreiincl  16719  joinfval  17463  meetfval  17477  dirge  17699  sylow2alem1  18497  efgredlemb  18625  kerf1ghm  19214  kerf1hrmOLD  19215  rmodislmodlem  19417  lbspss  19570  lspsneu  19611  lspsnat  19633  lspsncv0  19634  opsrtoslem2  19972  distop  21301  epttop  21315  isclo2  21394  restdis  21484  subbascn  21560  cnrest2  21592  cnpresti  21594  isnrm2  21664  cmpsublem  21705  cmpcld  21708  dfconn2  21725  t1connperf  21742  1stcrest  21759  lly1stc  21802  uptx  21931  txcn  21932  prdstopn  21934  txconn  21995  cmphaushmeo  22106  fbasrn  22190  csdfil  22200  trufil  22216  fclscf  22331  alexsubALTlem3  22355  alexsubALT  22357  haustsms2  22442  ovoliunlem1  23800  ovoliunnul  23805  volsup2  23903  coeaddlem  24536  plymul0or  24567  radcnv0  24701  wilthlem3  25343  chtub  25484  gausslemma2dlem1a  25637  2sqlem10  25700  pntpbnd1  25858  mptelee  26378  axeuclidlem  26445  axcontlem4  26450  elntg2  26468  uhgrissubgr  26754  finsumvtxdg2size  27029  wlkonl1iedg  27143  pthdivtx  27212  wlkiswwlksupgr2  27357  eucrct2eupthOLD  27770  eucrct2eupth  27771  isch3  28791  shmodsi  28941  orthin  28998  h1datomi  29133  stcltr2i  29827  atom1d  29905  sumdmdii  29967  cdj3lem1  29986  disjpreima  30094  lmxrge0  30830  dmvlsiga  31024  sibfof  31234  bnj600  31829  bnj1018  31872  bnj1173  31910  bnj1174  31911  erdszelem9  32021  cvmlift2lem1  32124  fundmpss  32499  tfisg  32546  frpoinsg  32572  frinsg  32578  poseq  32586  sltval2  32654  outsideofrflx  33079  nn0prpwlem  33161  ivthALT  33174  fnessref  33196  neibastop2lem  33199  tailfb  33216  bj-axtd  33412  bj-nfimt  33450  bj-nfdt0  33508  bj-sbievw2  33631  bj-2upleq  33807  bj-restn0  33856  icorempt2  34039  isbasisrelowllem2  34044  rdgellim  34064  rdgssun  34066  pibt2  34104  wl-ich-lem3  34217  wl-lem-moexsb  34223  matunitlindflem1  34307  poimirlem3  34314  poimirlem4  34315  poimirlem29  34340  mblfinlem3  34350  itg2addnclem3  34364  cover2  34409  fdc  34440  nninfnub  34446  equivtotbnd  34476  prdstotbnd  34492  cntotbnd  34494  ablo4pnp  34578  isdrngo3  34657  crngohomfo  34704  intidl  34727  or32dd  34794  iss2  35025  prtlem18  35436  prter2  35440  lsat0cv  35592  lfl1  35629  lkreqN  35729  atlrelat1  35880  pmaple  36320  pmapsub  36327  pclclN  36450  pclfinN  36459  osumcllem4N  36518  pexmidlem1N  36529  cdleme7ga  36807  lcfl7N  38060  rtprmirr  38604  ss2iundf  39345  brtrclfv2  39413  nzss  40042  3impexpbicom  40209  alrim3con13v  40263  tratrb  40266  onfrALTlem3  40274  onfrALTlem2  40276  onfrALTlem1  40278  trsspwALT2  40549  trsspwALT3  40550  or2expropbi  42653  afv2orxorb  42812  lswn0  42955  ich2exprop  42975  prproropf1olem4  43010  paireqne  43015  reupr  43026  lighneallem4b  43116  sbgoldbwt  43284  sbgoldbst  43285  sbgoldbalt  43288  isomuspgrlem1  43334  isomuspgrlem2d  43338  isupwlkg  43354  2zrngamgm  43548  fldivexpfllog2  43967  line2ylem  44080