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 ⊢ (𝜑 → (𝜓 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  3imtr4g  299  nic-ax  1706  sbequ1  2284  dfmoeu  2561  2moswapv  2655  mopick2  2663  2moswap  2670  2eu6  2682  necon3d  2977  necon1d  2978  ralrimd  3268  spcimegf  3515  spcegf  3547  spcimedv  3550  spc2gv  3555  spc3gv  3559  rspcimedv  3568  2reu1  3845  pwpw0  4774  sssn  4787  ssiun  5005  ssiun2  5006  replem  5241  wefrc  5645  ssrel  5759  dmcosseq  5960  dmcosseqOLD  5961  relssres  6013  trin2  6115  ssrnres  6169  sossfld  6177  reuop  6289  frpoinsg  6339  tron  6378  ordtri3or  6388  oneqmini  6409  fnun  6645  f1oun  6836  brprcneu  6867  brprcneuALT  6868  ssimaex  6962  chfnrn  7040  dffo4  7095  dffo5  7096  tpres  7199  fvclss  7237  isomin  7337  isofrlem  7340  isoselem  7341  fnoprabg  7535  tfisg  7854  nnsuc  7884  f1oweALT  7973  releldmdifi  8045  bropopvvv  8090  bropfvvvvlem  8091  frxp  8127  poxp  8129  fnse  8134  poseq  8159  mpoxopynvov0g  8215  issmo2  8341  smores  8344  smogt  8359  rdglim2  8424  onelfvnef1  8433  tz7.48lemOLD  8435  tz7.49  8439  swoer  8733  qsss  8780  domtriord  9126  findcard  9163  findcard2  9164  pssnn  9168  ssfiALT  9173  findcard3  9258  frfi  9260  dffi3  9407  supmo  9428  infmo  9473  inf3lem4  9616  frinsg  9739  carddom2  10039  fidomtri2  10056  pm54.43  10063  infpwfien  10122  alephordi  10134  cardaleph  10149  carduniima  10156  cardinfima  10157  alephval3  10170  dfac5lem4  10186  dfac5  10188  dfac2b  10190  kmlem2  10211  cflm  10308  cfslb2n  10327  cfsmolem  10329  isf32lem9  10420  axcc4  10498  domtriomlem  10501  zorn2lem4  10558  zorn2lem6  10560  fpwwe2lem10  10706  fpwwe2lem11  10707  inttsk  10840  inar1  10841  intgru  10880  ingru  10881  indpi  10973  nqpr  11080  ltaddpr  11100  ltexprlem1  11102  ltexprlem5  11106  reclem2pr  11114  reclem4pr  11116  negn0  11726  zmulcl  12726  uzm1  12980  uzwo  13019  xmullem2  13376  icoshft  13585  difreicc  13596  fzouzsplit  13809  ssfzoulel  13875  seqf1olem1  14164  seqf1olem2  14165  hashge2el2difr  14606  hashtpg  14610  reusq0  15612  modfsummod  15941  incexclem  15985  sqrt2irr  16397  dvds2lem  16418  dvdslelem  16459  oddnn02np1  16498  divalglem8  16550  dfgcd2  16699  2mulprm  16848  ge2nprmge4  16857  euclemma  16869  iserodd  16993  ramcl  17187  setsstruct  17334  mreiincl  17746  joinfval  18525  meetfval  18539  dirge  18757  chnccat  18780  kerf1ghm  19441  sylow2alem1  19811  efgredlemb  19940  crngrhmfo  20706  isdomn4  20947  isdrng5  20988  rmodislmodlem  21184  lbspss  21337  lspsneu  21381  lspsnat  21403  lspsncv0  21404  opsrtoslem2  22345  matunitlindflem1  22974  distop  23293  epttop  23307  isclo2  23386  restdis  23476  subbascn  23552  cnrest2  23584  cnpresti  23586  isnrm2  23656  cmpsublem  23697  cmpcld  23700  dfconn2  23717  t1connperf  23734  1stcrest  23751  lly1stc  23795  uptx  23924  txcn  23925  prdstopn  23927  txconn  23988  cmphaushmeo  24099  fbasrn  24183  csdfil  24193  trufil  24209  fclscf  24324  alexsubALTlem3  24348  alexsubALT  24350  haustsms2  24436  ovoliunlem1  25803  ovoliunnul  25808  volsup2  25906  coeaddlem  26548  plymul0or  26581  radcnv0  26725  rtprmirr  27070  wilthlem3  27379  chtub  27521  gausslemma2dlem1a  27674  2sqlem10  27737  pntpbnd1  27895  ltsval2  27995  noetalem1  28080  bday1  28182  mpteleeOLD  29455  axeuclidlem  29522  axcontlem4  29527  elntg2  29545  uhgrissubgr  29838  finsumvtxdg2size  30113  wlkonl1iedg  30226  subgrwlk  30251  pthdivtx  30294  pthisspthorcycl  30372  wlkiswwlksupgr2  30448  eucrct2eupth  30828  isch3  31825  shmodsi  31973  orthin  32030  h1datomi  32165  stcltr2i  32859  atom1d  32937  sumdmdii  32999  cdj3lem1  33018  disjpreima  33160  lmxrge0  34566  dmvlsiga  34743  sibfof  34955  bnj600  35532  bnj1018g  35576  bnj1018  35577  bnj1173  35615  bnj1174  35616  fnfvintima  35695  trssfir1om  35716  trssfir1omregs  35777  karddom  35802  kardsdom  35803  onvf1odlem2  35856  onvf1odlem4  35858  cusgracyclt3v  35890  erdszelem9  35933  cvmlift2lem1  36036  satfvsucsuc  36099  sat1el2xp  36113  fmla0xp  36117  3jcadALT  36421  fundmpss  36501  outsideofrflx  36862  nn0prpwlem  37080  ivthALT  37093  fnessref  37115  neibastop2lem  37118  tailfb  37135  bj-axtd  37434  bj-nfimt  37492  bj-nfdt0  37567  bj-nnfand  37627  bj-sbievw2  37728  bj-2upleq  37895  bj-restn0  37979  icorempo  38242  isbasisrelowllem2  38247  rdgellim  38267  rdgssun  38269  pibt2  38308  wl-lem-moexsb  38468  poimirlem3  38509  poimirlem4  38510  poimirlem29  38535  mblfinlem3  38545  itg2addnclem3  38559  cover2  38617  fdc  38647  nninfnub  38653  equivtotbnd  38680  prdstotbnd  38696  cntotbnd  38698  ablo4pnp  38782  isdrngo3  38861  crngohomfo  38908  intidl  38931  or32dd  38994  iss2  39244  refressn  39433  eldisjlem19  39813  prtlem18  39902  prter2  39906  lsat0cv  40058  lfl1  40095  lkreqN  40195  atlrelat1  40346  pmapsub  40793  pclclN  40916  pclfinN  40925  osumcllem4N  40984  pexmidlem1N  40995  cdleme7ga  41273  lcfl7N  42526  eu6w  43641  dflim5  44289  omabs2  44292  ss2iundf  44618  brtrclfv2  44686  ismnushort  45244  nzss  45260  3impexpbicom  45422  alrim3con13v  45475  tratrb  45478  onfrALTlem3  45486  onfrALTlem2  45488  onfrALTlem1  45490  trsspwALT2  45760  trsspwALT3  45761  relpmin  45894  relpfrlem  45895  trfr  45904  or2expropbi  48048  afv2orxorb  48242  lswn0  48470  ich2exprop  48497  prproropf1olem4  48532  paireqne  48537  reupr  48548  lighneallem4b  48638  sbgoldbwt  48819  sbgoldbst  48820  sbgoldbalt  48823  cycldlenngric  48970  isupwlkg  49179  2zrngamgm  49286  fldivexpfllog2  49621  line2ylem  49807  fdomne0  49904