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  1673  sbequ1  2249  dfmoeu  2529  2moswapv  2622  mopick2  2630  2moswap  2637  2eu6  2650  necon3d  2946  necon1d  2947  ralrimd  3234  spcimegf  3508  spcegf  3549  spcimedv  3552  spc2gv  3557  spc3gv  3561  rspcimedv  3570  2reu1  3851  pwpw0  4767  sssn  4780  ssiun  4998  ssiun2  4999  wefrc  5617  ssrel  5730  dmcosseq  5923  dmcosseqOLD  5924  dmcosseqOLDOLD  5925  relssres  5977  trin2  6076  ssrnres  6131  sossfld  6139  reuop  6245  frpoinsg  6295  tron  6334  ordtri3or  6343  oneqmini  6364  fnun  6600  f1oun  6787  brprcneu  6816  brprcneuALT  6817  ssimaex  6912  chfnrn  6987  dffo4  7041  dffo5  7042  tpres  7141  fvclss  7181  isomin  7278  isofrlem  7281  isoselem  7282  fnoprabg  7476  tfisg  7794  nnsuc  7824  f1oweALT  7914  releldmdifi  7987  bropopvvv  8030  bropfvvvvlem  8031  frxp  8066  poxp  8068  fnse  8073  poseq  8098  mpoxopynvov0g  8154  issmo2  8279  smores  8282  smogt  8297  rdglim2  8361  tz7.48lem  8370  tz7.49  8374  swoer  8663  qsss  8710  domtriord  9047  findcard  9087  findcard2  9088  pssnn  9092  ssfiALT  9098  findcard3  9187  findcard3OLD  9188  frfi  9190  dffi3  9340  supmo  9361  infmo  9406  inf3lem4  9546  frinsg  9666  carddom2  9892  fidomtri2  9909  pm54.43  9916  infpwfien  9975  alephordi  9987  cardaleph  10002  carduniima  10009  cardinfima  10010  alephval3  10023  dfac5lem4  10039  dfac5lem4OLD  10041  dfac5  10042  dfac2b  10044  kmlem2  10065  cflm  10163  cfslb2n  10181  cfsmolem  10183  isf32lem9  10274  axcc4  10352  domtriomlem  10355  zorn2lem4  10412  zorn2lem6  10414  fpwwe2lem10  10553  fpwwe2lem11  10554  inttsk  10687  inar1  10688  intgru  10727  ingru  10728  indpi  10820  nqpr  10927  ltaddpr  10947  ltexprlem1  10949  ltexprlem5  10953  reclem2pr  10961  reclem4pr  10963  negn0  11567  zmulcl  12542  uzm1  12791  uzwo  12830  xmullem2  13185  icoshft  13394  difreicc  13405  fzouzsplit  13615  ssfzoulel  13681  seqf1olem1  13966  seqf1olem2  13967  hashge2el2difr  14406  hashtpg  14410  reusq0  15390  modfsummod  15719  incexclem  15761  sqrt2irr  16176  dvds2lem  16197  dvdslelem  16238  oddnn02np1  16277  divalglem8  16329  dfgcd2  16475  2mulprm  16622  ge2nprmge4  16630  euclemma  16642  iserodd  16765  ramcl  16959  setsstruct  17105  mreiincl  17516  joinfval  18295  meetfval  18309  dirge  18527  kerf1ghm  19144  sylow2alem1  19514  efgredlemb  19643  isdomn4  20619  rmodislmodlem  20850  lbspss  21004  lspsneu  21048  lspsnat  21070  lspsncv0  21071  opsrtoslem2  21979  distop  22898  epttop  22912  isclo2  22991  restdis  23081  subbascn  23157  cnrest2  23189  cnpresti  23191  isnrm2  23261  cmpsublem  23302  cmpcld  23305  dfconn2  23322  t1connperf  23339  1stcrest  23356  lly1stc  23399  uptx  23528  txcn  23529  prdstopn  23531  txconn  23592  cmphaushmeo  23703  fbasrn  23787  csdfil  23797  trufil  23813  fclscf  23928  alexsubALTlem3  23952  alexsubALT  23954  haustsms2  24040  ovoliunlem1  25419  ovoliunnul  25424  volsup2  25522  coeaddlem  26170  plymul0or  26204  radcnv0  26341  rtprmirr  26686  wilthlem3  26996  chtub  27139  gausslemma2dlem1a  27292  2sqlem10  27355  pntpbnd1  27513  sltval2  27584  noetalem1  27669  bday1s  27763  mptelee  28858  axeuclidlem  28925  axcontlem4  28930  elntg2  28948  uhgrissubgr  29238  finsumvtxdg2size  29514  wlkonl1iedg  29627  pthdivtx  29690  pthisspthorcycl  29765  wlkiswwlksupgr2  29840  eucrct2eupth  30207  isch3  31203  shmodsi  31351  orthin  31408  h1datomi  31543  stcltr2i  32237  atom1d  32315  sumdmdii  32377  cdj3lem1  32396  disjpreima  32546  lmxrge0  33918  dmvlsiga  34095  sibfof  34307  bnj600  34885  bnj1018g  34929  bnj1018  34930  bnj1173  34968  bnj1174  34969  onvf1odlem2  35076  onvf1odlem4  35078  subgrwlk  35104  cusgracyclt3v  35128  erdszelem9  35171  cvmlift2lem1  35274  satfvsucsuc  35337  sat1el2xp  35351  fmla0xp  35355  3jcadALT  35659  fundmpss  35739  outsideofrflx  36100  nn0prpwlem  36295  ivthALT  36308  fnessref  36330  neibastop2lem  36333  tailfb  36350  bj-axtd  36567  bj-nfimt  36611  bj-nfdt0  36668  bj-nnfand  36722  bj-sbievw2  36819  bj-2upleq  36985  bj-restn0  37063  icorempo  37324  isbasisrelowllem2  37329  rdgellim  37349  rdgssun  37351  pibt2  37390  wl-lem-moexsb  37541  matunitlindflem1  37595  poimirlem3  37602  poimirlem4  37603  poimirlem29  37628  mblfinlem3  37638  itg2addnclem3  37652  cover2  37694  fdc  37724  nninfnub  37730  equivtotbnd  37757  prdstotbnd  37773  cntotbnd  37775  ablo4pnp  37859  isdrngo3  37938  crngohomfo  37985  intidl  38008  or32dd  38073  iss2  38311  refressn  38419  eldisjlem19  38787  prtlem18  38855  prter2  38859  lsat0cv  39011  lfl1  39048  lkreqN  39148  atlrelat1  39299  pmaple  39740  pmapsub  39747  pclclN  39870  pclfinN  39879  osumcllem4N  39938  pexmidlem1N  39949  cdleme7ga  40227  lcfl7N  41480  eu6w  42649  dflim5  43302  omabs2  43305  ss2iundf  43632  brtrclfv2  43700  ismnushort  44274  nzss  44290  3impexpbicom  44454  alrim3con13v  44507  tratrb  44510  onfrALTlem3  44518  onfrALTlem2  44520  onfrALTlem1  44522  trsspwALT2  44792  trsspwALT3  44793  relpmin  44926  relpfrlem  44927  trfr  44936  or2expropbi  47019  afv2orxorb  47213  lswn0  47429  ich2exprop  47456  prproropf1olem4  47491  paireqne  47496  reupr  47507  lighneallem4b  47594  sbgoldbwt  47762  sbgoldbst  47763  sbgoldbalt  47766  cycldlenngric  47913  isupwlkg  48122  2zrngamgm  48230  fldivexpfllog2  48551  line2ylem  48737  fdomne0  48835