Theorem imbitrrdi 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, 5-Aug-1993.)

Hypotheses

Ref	Expression
imbitrrdi.1	⊢ (𝜑 → (𝜓 → 𝜒))
imbitrrdi.2	⊢ (𝜃 ↔ 𝜒)

Assertion

Ref	Expression
imbitrrdi	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem imbitrrdi

Step	Hyp	Ref	Expression
1		imbitrrdi.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		imbitrrdi.2	. . 3 ⊢ (𝜃 ↔ 𝜒)
3	2	biimpri 231	. 2 ⊢ (𝜒 → 𝜃)
4	1, 3	syl6 36	1 ⊢ (𝜑 → (𝜓 → 𝜃))

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  1703  sbequ1  2284  dfmoeu  2563  2moswapv  2657  mopick2  2665  2moswap  2672  2eu6  2684  necon3d  2979  necon1d  2980  ralrimd  3270  spcimegf  3520  spcegf  3552  spcimedv  3555  spc2gv  3560  spc3gv  3564  rspcimedv  3573  2reu1  3852  pwpw0  4780  sssn  4793  ssiun  5012  ssiun2  5013  replem  5250  wefrc  5657  ssrel  5771  dmcosseq  5970  dmcosseqOLD  5971  relssres  6023  trin2  6125  ssrnres  6178  sossfld  6186  reuop  6296  frpoinsg  6346  tron  6385  ordtri3or  6395  oneqmini  6416  fnun  6651  f1oun  6842  brprcneu  6873  brprcneuALT  6874  ssimaex  6968  chfnrn  7046  dffo4  7100  dffo5  7101  tpres  7201  fvclss  7241  isomin  7337  isofrlem  7340  isoselem  7341  fnoprabg  7535  tfisg  7851  nnsuc  7881  f1oweALT  7970  releldmdifi  8043  bropopvvv  8086  bropfvvvvlem  8087  frxp  8123  poxp  8125  fnse  8130  poseq  8155  mpoxopynvov0g  8211  issmo2  8337  smores  8340  smogt  8355  rdglim2  8420  tz7.48lem  8429  tz7.49  8433  swoer  8727  qsss  8774  domtriord  9112  findcard  9149  findcard2  9150  pssnn  9154  ssfiALT  9159  findcard3  9244  frfi  9246  dffi3  9392  supmo  9413  infmo  9458  inf3lem4  9601  frinsg  9724  carddom2  9964  fidomtri2  9981  pm54.43  9988  infpwfien  10047  alephordi  10059  cardaleph  10074  carduniima  10081  cardinfima  10082  alephval3  10095  dfac5lem4  10111  dfac5  10113  dfac2b  10115  kmlem2  10136  cflm  10234  cfslb2n  10253  cfsmolem  10255  isf32lem9  10346  axcc4  10424  domtriomlem  10427  zorn2lem4  10484  zorn2lem6  10486  fpwwe2lem10  10626  fpwwe2lem11  10627  inttsk  10760  inar1  10761  intgru  10800  ingru  10801  indpi  10893  nqpr  11000  ltaddpr  11020  ltexprlem1  11022  ltexprlem5  11026  reclem2pr  11034  reclem4pr  11036  negn0  11644  zmulcl  12644  uzm1  12897  uzwo  12936  xmullem2  13292  icoshft  13501  difreicc  13512  fzouzsplit  13725  ssfzoulel  13791  seqf1olem1  14079  seqf1olem2  14080  hashge2el2difr  14520  hashtpg  14524  reusq0  15518  modfsummod  15848  incexclem  15892  sqrt2irr  16306  dvds2lem  16327  dvdslelem  16368  oddnn02np1  16407  divalglem8  16459  dfgcd2  16605  2mulprm  16752  ge2nprmge4  16761  euclemma  16773  iserodd  16896  ramcl  17090  setsstruct  17237  mreiincl  17649  joinfval  18428  meetfval  18442  dirge  18660  chnccat  18683  kerf1ghm  19318  sylow2alem1  19688  efgredlemb  19817  isdomn4  20801  rmodislmodlem  21031  lbspss  21184  lspsneu  21228  lspsnat  21250  lspsncv0  21251  opsrtoslem2  22188  distop  23133  epttop  23147  isclo2  23226  restdis  23316  subbascn  23392  cnrest2  23424  cnpresti  23426  isnrm2  23496  cmpsublem  23537  cmpcld  23540  dfconn2  23557  t1connperf  23574  1stcrest  23591  lly1stc  23634  uptx  23763  txcn  23764  prdstopn  23766  txconn  23827  cmphaushmeo  23938  fbasrn  24022  csdfil  24032  trufil  24048  fclscf  24163  alexsubALTlem3  24187  alexsubALT  24189  haustsms2  24275  ovoliunlem1  25642  ovoliunnul  25647  volsup2  25745  coeaddlem  26387  plymul0or  26420  radcnv0  26560  rtprmirr  26906  wilthlem3  27215  chtub  27357  gausslemma2dlem1a  27510  2sqlem10  27573  pntpbnd1  27731  ltsval2  27801  noetalem1  27886  bday1  27988  mpteleeOLD  29226  axeuclidlem  29293  axcontlem4  29298  elntg2  29316  uhgrissubgr  29606  finsumvtxdg2size  29881  wlkonl1iedg  29994  pthdivtx  30057  pthisspthorcycl  30132  wlkiswwlksupgr2  30207  eucrct2eupth  30577  isch3  31574  shmodsi  31722  orthin  31779  h1datomi  31914  stcltr2i  32608  atom1d  32686  sumdmdii  32748  cdj3lem1  32767  disjpreima  32910  lmxrge0  34323  dmvlsiga  34500  sibfof  34711  bnj600  35288  bnj1018g  35332  bnj1018  35333  bnj1173  35371  bnj1174  35372  fnfvintima  35457  trssfir1om  35488  trssfir1omregs  35530  karddom  35555  kardsdom  35556  onvf1odlem2  35569  onvf1odlem4  35571  subgrwlk  35605  cusgracyclt3v  35629  erdszelem9  35672  cvmlift2lem1  35775  satfvsucsuc  35838  sat1el2xp  35852  fmla0xp  35856  3jcadALT  36160  fundmpss  36240  outsideofrflx  36600  nn0prpwlem  36814  ivthALT  36827  fnessref  36849  neibastop2lem  36852  tailfb  36869  mh-inf3f1  37033  bj-axtd  37168  bj-nfimt  37226  bj-nfdt0  37301  bj-nnfand  37361  bj-sbievw2  37462  bj-2upleq  37629  bj-restn0  37713  icorempo  37978  isbasisrelowllem2  37983  rdgellim  38003  rdgssun  38005  pibt2  38044  wl-lem-moexsb  38204  matunitlindflem1  38248  poimirlem3  38255  poimirlem4  38256  poimirlem29  38281  mblfinlem3  38291  itg2addnclem3  38305  cover2  38347  fdc  38377  nninfnub  38383  equivtotbnd  38410  prdstotbnd  38426  cntotbnd  38428  ablo4pnp  38512  isdrngo3  38591  crngohomfo  38638  intidl  38661  or32dd  38724  iss2  38974  refressn  39163  eldisjlem19  39543  prtlem18  39632  prter2  39636  lsat0cv  39788  lfl1  39825  lkreqN  39925  atlrelat1  40076  pmapsub  40523  pclclN  40646  pclfinN  40655  osumcllem4N  40714  pexmidlem1N  40725  cdleme7ga  41003  lcfl7N  42256  eu6w  43391  dflim5  44039  omabs2  44042  ss2iundf  44368  brtrclfv2  44436  ismnushort  44994  nzss  45010  3impexpbicom  45172  alrim3con13v  45225  tratrb  45228  onfrALTlem3  45236  onfrALTlem2  45238  onfrALTlem1  45240  trsspwALT2  45510  trsspwALT3  45511  relpmin  45644  relpfrlem  45645  trfr  45654  or2expropbi  47754  afv2orxorb  47948  lswn0  48176  ich2exprop  48203  prproropf1olem4  48238  paireqne  48243  reupr  48254  lighneallem4b  48344  sbgoldbwt  48525  sbgoldbst  48526  sbgoldbalt  48529  cycldlenngric  48676  isupwlkg  48885  2zrngamgm  48993  fldivexpfllog2  49328  line2ylem  49514  fdomne0  49611