Theorem imbitrrdi 252

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  3imtr4g  296  nic-ax  1674  sbequ1  2251  dfmoeu  2531  2moswapv  2624  mopick2  2632  2moswap  2639  2eu6  2652  necon3d  2949  necon1d  2950  ralrimd  3237  spcimegf  3506  spcegf  3547  spcimedv  3550  spc2gv  3555  spc3gv  3559  rspcimedv  3568  2reu1  3848  pwpw0  4765  sssn  4778  ssiun  4995  ssiun2  4996  wefrc  5610  ssrel  5723  dmcosseq  5917  dmcosseqOLD  5918  dmcosseqOLDOLD  5919  relssres  5971  trin2  6070  ssrnres  6125  sossfld  6133  reuop  6240  frpoinsg  6290  tron  6329  ordtri3or  6338  oneqmini  6359  fnun  6595  f1oun  6782  brprcneu  6812  brprcneuALT  6813  ssimaex  6907  chfnrn  6982  dffo4  7036  dffo5  7037  tpres  7135  fvclss  7175  isomin  7271  isofrlem  7274  isoselem  7275  fnoprabg  7469  tfisg  7784  nnsuc  7814  f1oweALT  7904  releldmdifi  7977  bropopvvv  8020  bropfvvvvlem  8021  frxp  8056  poxp  8058  fnse  8063  poseq  8088  mpoxopynvov0g  8144  issmo2  8269  smores  8272  smogt  8287  rdglim2  8351  tz7.48lem  8360  tz7.49  8364  swoer  8653  qsss  8700  domtriord  9036  findcard  9073  findcard2  9074  pssnn  9078  ssfiALT  9083  findcard3  9167  frfi  9169  dffi3  9315  supmo  9336  infmo  9381  inf3lem4  9521  frinsg  9641  carddom2  9867  fidomtri2  9884  pm54.43  9891  infpwfien  9950  alephordi  9962  cardaleph  9977  carduniima  9984  cardinfima  9985  alephval3  9998  dfac5lem4  10014  dfac5lem4OLD  10016  dfac5  10017  dfac2b  10019  kmlem2  10040  cflm  10138  cfslb2n  10156  cfsmolem  10158  isf32lem9  10249  axcc4  10327  domtriomlem  10330  zorn2lem4  10387  zorn2lem6  10389  fpwwe2lem10  10528  fpwwe2lem11  10529  inttsk  10662  inar1  10663  intgru  10702  ingru  10703  indpi  10795  nqpr  10902  ltaddpr  10922  ltexprlem1  10924  ltexprlem5  10928  reclem2pr  10936  reclem4pr  10938  negn0  11543  zmulcl  12518  uzm1  12767  uzwo  12806  xmullem2  13161  icoshft  13370  difreicc  13381  fzouzsplit  13591  ssfzoulel  13657  seqf1olem1  13945  seqf1olem2  13946  hashge2el2difr  14385  hashtpg  14389  reusq0  15369  modfsummod  15698  incexclem  15740  sqrt2irr  16155  dvds2lem  16176  dvdslelem  16217  oddnn02np1  16256  divalglem8  16308  dfgcd2  16454  2mulprm  16601  ge2nprmge4  16609  euclemma  16621  iserodd  16744  ramcl  16938  setsstruct  17084  mreiincl  17495  joinfval  18274  meetfval  18288  dirge  18506  chnccat  18529  kerf1ghm  19157  sylow2alem1  19527  efgredlemb  19656  isdomn4  20629  rmodislmodlem  20860  lbspss  21014  lspsneu  21058  lspsnat  21080  lspsncv0  21081  opsrtoslem2  21989  distop  22908  epttop  22922  isclo2  23001  restdis  23091  subbascn  23167  cnrest2  23199  cnpresti  23201  isnrm2  23271  cmpsublem  23312  cmpcld  23315  dfconn2  23332  t1connperf  23349  1stcrest  23366  lly1stc  23409  uptx  23538  txcn  23539  prdstopn  23541  txconn  23602  cmphaushmeo  23713  fbasrn  23797  csdfil  23807  trufil  23823  fclscf  23938  alexsubALTlem3  23962  alexsubALT  23964  haustsms2  24050  ovoliunlem1  25428  ovoliunnul  25433  volsup2  25531  coeaddlem  26179  plymul0or  26213  radcnv0  26350  rtprmirr  26695  wilthlem3  27005  chtub  27148  gausslemma2dlem1a  27301  2sqlem10  27364  pntpbnd1  27522  sltval2  27593  noetalem1  27678  bday1s  27773  mptelee  28871  axeuclidlem  28938  axcontlem4  28943  elntg2  28961  uhgrissubgr  29251  finsumvtxdg2size  29527  wlkonl1iedg  29640  pthdivtx  29703  pthisspthorcycl  29778  wlkiswwlksupgr2  29853  eucrct2eupth  30220  isch3  31216  shmodsi  31364  orthin  31421  h1datomi  31556  stcltr2i  32250  atom1d  32328  sumdmdii  32390  cdj3lem1  32409  disjpreima  32559  lmxrge0  33960  dmvlsiga  34137  sibfof  34348  bnj600  34926  bnj1018g  34970  bnj1018  34971  bnj1173  35009  bnj1174  35010  trssfir1omregs  35120  onvf1odlem2  35136  onvf1odlem4  35138  subgrwlk  35164  cusgracyclt3v  35188  erdszelem9  35231  cvmlift2lem1  35334  satfvsucsuc  35397  sat1el2xp  35411  fmla0xp  35415  3jcadALT  35719  fundmpss  35799  outsideofrflx  36160  nn0prpwlem  36355  ivthALT  36368  fnessref  36390  neibastop2lem  36393  tailfb  36410  bj-axtd  36627  bj-nfimt  36671  bj-nfdt0  36728  bj-nnfand  36782  bj-sbievw2  36879  bj-2upleq  37045  bj-restn0  37123  icorempo  37384  isbasisrelowllem2  37389  rdgellim  37409  rdgssun  37411  pibt2  37450  wl-lem-moexsb  37601  matunitlindflem1  37655  poimirlem3  37662  poimirlem4  37663  poimirlem29  37688  mblfinlem3  37698  itg2addnclem3  37712  cover2  37754  fdc  37784  nninfnub  37790  equivtotbnd  37817  prdstotbnd  37833  cntotbnd  37835  ablo4pnp  37919  isdrngo3  37998  crngohomfo  38045  intidl  38068  or32dd  38133  iss2  38371  refressn  38479  eldisjlem19  38847  prtlem18  38915  prter2  38919  lsat0cv  39071  lfl1  39108  lkreqN  39208  atlrelat1  39359  pmaple  39799  pmapsub  39806  pclclN  39929  pclfinN  39938  osumcllem4N  39997  pexmidlem1N  40008  cdleme7ga  40286  lcfl7N  41539  eu6w  42708  dflim5  43361  omabs2  43364  ss2iundf  43691  brtrclfv2  43759  ismnushort  44333  nzss  44349  3impexpbicom  44512  alrim3con13v  44565  tratrb  44568  onfrALTlem3  44576  onfrALTlem2  44578  onfrALTlem1  44580  trsspwALT2  44850  trsspwALT3  44851  relpmin  44984  relpfrlem  44985  trfr  44994  or2expropbi  47064  afv2orxorb  47258  lswn0  47474  ich2exprop  47501  prproropf1olem4  47536  paireqne  47541  reupr  47552  lighneallem4b  47639  sbgoldbwt  47807  sbgoldbst  47808  sbgoldbalt  47811  cycldlenngric  47958  isupwlkg  48167  2zrngamgm  48275  fldivexpfllog2  48596  line2ylem  48782  fdomne0  48880