Theorem syl6ibr 251

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 227	. 2 ⊢ (𝜒 → 𝜃)
4	1, 3	syl6 35	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  3imtr4g  295  nic-ax  1677  sbequ1  2243  dfmoeu  2536  2moswapv  2631  mopick2  2639  2moswap  2646  2eu6  2658  necon3d  2963  necon1d  2964  ralrimd  3141  spcimegf  3519  spcegf  3521  spcimedv  3524  spc2gv  3529  spc3gv  3533  rspcimedv  3542  2reu1  3826  pwpw0  4743  sssn  4756  pwsnOLD  4829  ssiun  4972  ssiun2  4973  wefrc  5574  ssrel  5683  dmcosseq  5871  relssres  5921  trin2  6017  ssrnres  6070  sossfld  6078  reuop  6185  frpoinsg  6231  wfisgOLD  6242  tron  6274  ordtri3or  6283  oneqmini  6302  fnun  6529  f1oun  6719  brprcneu  6747  fvprc  6748  ssimaex  6835  chfnrn  6908  dffo4  6961  dffo5  6962  tpres  7058  fvclss  7097  isomin  7188  isofrlem  7191  isoselem  7192  fnoprabg  7375  nnsuc  7705  f1oweALT  7788  releldmdifi  7859  bropopvvv  7901  bropfvvvvlem  7902  frxp  7938  poxp  7940  fnse  7945  mpoxopynvov0g  8001  issmo2  8151  smores  8154  smogt  8169  rdglim2  8234  tz7.48lem  8242  tz7.49  8246  swoer  8486  qsss  8525  domtriord  8859  findcard  8908  findcard2  8909  pssnn  8913  ssfiALT  8919  pssnnOLD  8969  findcard2OLD  8986  findcard3  8987  frfi  8989  dffi3  9120  supmo  9141  infmo  9184  inf3lem4  9319  frinsg  9440  carddom2  9666  fidomtri2  9683  pm54.43  9690  infpwfien  9749  alephordi  9761  cardaleph  9776  carduniima  9783  cardinfima  9784  alephval3  9797  dfac5lem4  9813  dfac5  9815  dfac2b  9817  kmlem2  9838  cflm  9937  cfslb2n  9955  cfsmolem  9957  isf32lem9  10048  axcc4  10126  domtriomlem  10129  zorn2lem4  10186  zorn2lem6  10188  fpwwe2lem10  10327  fpwwe2lem11  10328  inttsk  10461  inar1  10462  intgru  10501  ingru  10502  indpi  10594  nqpr  10701  ltaddpr  10721  ltexprlem1  10723  ltexprlem5  10727  reclem2pr  10735  reclem4pr  10737  negn0  11334  zmulcl  12299  uzm1  12545  uzwo  12580  xmullem2  12928  icoshft  13134  difreicc  13145  fzouzsplit  13350  ssfzoulel  13409  seqf1olem1  13690  seqf1olem2  13691  hashge2el2difr  14123  hashtpg  14127  reusq0  15102  modfsummod  15434  incexclem  15476  sqrt2irr  15886  dvds2lem  15906  dvdslelem  15946  oddnn02np1  15985  divalglem8  16037  dfgcd2  16182  2mulprm  16326  ge2nprmge4  16334  euclemma  16346  iserodd  16464  ramcl  16658  setsstruct  16805  mreiincl  17222  joinfval  18006  meetfval  18020  dirge  18236  sylow2alem1  19137  efgredlemb  19267  kerf1ghm  19902  rmodislmodlem  20105  lbspss  20259  lspsneu  20300  lspsnat  20322  lspsncv0  20323  opsrtoslem2  21173  distop  22053  epttop  22067  isclo2  22147  restdis  22237  subbascn  22313  cnrest2  22345  cnpresti  22347  isnrm2  22417  cmpsublem  22458  cmpcld  22461  dfconn2  22478  t1connperf  22495  1stcrest  22512  lly1stc  22555  uptx  22684  txcn  22685  prdstopn  22687  txconn  22748  cmphaushmeo  22859  fbasrn  22943  csdfil  22953  trufil  22969  fclscf  23084  alexsubALTlem3  23108  alexsubALT  23110  haustsms2  23196  ovoliunlem1  24571  ovoliunnul  24576  volsup2  24674  coeaddlem  25315  plymul0or  25346  radcnv0  25480  wilthlem3  26124  chtub  26265  gausslemma2dlem1a  26418  2sqlem10  26481  pntpbnd1  26639  mptelee  27166  axeuclidlem  27233  axcontlem4  27238  elntg2  27256  uhgrissubgr  27545  finsumvtxdg2size  27820  wlkonl1iedg  27935  pthdivtx  27998  wlkiswwlksupgr2  28143  eucrct2eupth  28510  isch3  29504  shmodsi  29652  orthin  29709  h1datomi  29844  stcltr2i  30538  atom1d  30616  sumdmdii  30678  cdj3lem1  30697  disjpreima  30824  lmxrge0  31804  dmvlsiga  31997  sibfof  32207  bnj600  32799  bnj1018g  32843  bnj1018  32844  bnj1173  32882  bnj1174  32883  pthisspthorcycl  32990  subgrwlk  32994  cusgracyclt3v  33018  erdszelem9  33061  cvmlift2lem1  33164  satfvsucsuc  33227  sat1el2xp  33241  fmla0xp  33245  fundmpss  33646  tfisg  33692  poseq  33729  sltval2  33786  noetalem1  33871  bday1s  33952  outsideofrflx  34356  nn0prpwlem  34438  ivthALT  34451  fnessref  34473  neibastop2lem  34476  tailfb  34493  bj-axtd  34703  bj-nfimt  34746  bj-nfdt0  34804  bj-nnfand  34858  bj-sbievw2  34957  bj-2upleq  35129  bj-restn0  35188  icorempo  35449  isbasisrelowllem2  35454  rdgellim  35474  rdgssun  35476  pibt2  35515  wl-lem-moexsb  35650  matunitlindflem1  35700  poimirlem3  35707  poimirlem4  35708  poimirlem29  35733  mblfinlem3  35743  itg2addnclem3  35757  cover2  35799  fdc  35830  nninfnub  35836  equivtotbnd  35863  prdstotbnd  35879  cntotbnd  35881  ablo4pnp  35965  isdrngo3  36044  crngohomfo  36091  intidl  36114  or32dd  36179  iss2  36406  prtlem18  36818  prter2  36822  lsat0cv  36974  lfl1  37011  lkreqN  37111  atlrelat1  37262  pmaple  37702  pmapsub  37709  pclclN  37832  pclfinN  37841  osumcllem4N  37900  pexmidlem1N  37911  cdleme7ga  38189  lcfl7N  39442  isdomn4  40100  rtprmirr  40268  ss2iundf  41156  brtrclfv2  41224  ismnushort  41808  nzss  41824  3impexpbicom  41988  alrim3con13v  42042  tratrb  42045  onfrALTlem3  42053  onfrALTlem2  42055  onfrALTlem1  42057  trsspwALT2  42328  trsspwALT3  42329  or2expropbi  44415  afv2orxorb  44607  lswn0  44784  ich2exprop  44811  prproropf1olem4  44846  paireqne  44851  reupr  44862  lighneallem4b  44949  sbgoldbwt  45117  sbgoldbst  45118  sbgoldbalt  45121  isomuspgrlem1  45167  isomuspgrlem2d  45171  isupwlkg  45187  2zrngamgm  45385  fldivexpfllog2  45799  line2ylem  45985  fdomne0  46065