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  1672  sbequ1  2247  dfmoeu  2535  2moswapv  2628  mopick2  2636  2moswap  2643  2eu6  2656  necon3d  2960  necon1d  2961  ralrimd  3263  spcimegf  3550  spcegf  3591  spcimedv  3594  spc2gv  3599  spc3gv  3603  rspcimedv  3612  2reu1  3896  pwpw0  4812  sssn  4825  ssiun  5045  ssiun2  5046  wefrc  5678  ssrel  5791  ssrelOLD  5792  dmcosseq  5986  dmcosseqOLD  5987  relssres  6039  trin2  6142  ssrnres  6197  sossfld  6205  reuop  6312  frpoinsg  6363  wfisgOLD  6374  tron  6406  ordtri3or  6415  oneqmini  6435  fnun  6681  f1oun  6866  brprcneu  6895  brprcneuALT  6896  ssimaex  6993  chfnrn  7068  dffo4  7122  dffo5  7123  tpres  7222  fvclss  7262  isomin  7358  isofrlem  7361  isoselem  7362  fnoprabg  7557  tfisg  7876  nnsuc  7906  f1oweALT  7998  releldmdifi  8071  bropopvvv  8116  bropfvvvvlem  8117  frxp  8152  poxp  8154  fnse  8159  poseq  8184  mpoxopynvov0g  8240  issmo2  8390  smores  8393  smogt  8408  rdglim2  8473  tz7.48lem  8482  tz7.49  8486  swoer  8777  qsss  8819  domtriord  9164  findcard  9204  findcard2  9205  pssnn  9209  ssfiALT  9215  findcard3  9319  findcard3OLD  9320  frfi  9322  dffi3  9472  supmo  9493  infmo  9536  inf3lem4  9672  frinsg  9792  carddom2  10018  fidomtri2  10035  pm54.43  10042  infpwfien  10103  alephordi  10115  cardaleph  10130  carduniima  10137  cardinfima  10138  alephval3  10151  dfac5lem4  10167  dfac5lem4OLD  10169  dfac5  10170  dfac2b  10172  kmlem2  10193  cflm  10291  cfslb2n  10309  cfsmolem  10311  isf32lem9  10402  axcc4  10480  domtriomlem  10483  zorn2lem4  10540  zorn2lem6  10542  fpwwe2lem10  10681  fpwwe2lem11  10682  inttsk  10815  inar1  10816  intgru  10855  ingru  10856  indpi  10948  nqpr  11055  ltaddpr  11075  ltexprlem1  11077  ltexprlem5  11081  reclem2pr  11089  reclem4pr  11091  negn0  11693  zmulcl  12668  uzm1  12917  uzwo  12954  xmullem2  13308  icoshft  13514  difreicc  13525  fzouzsplit  13735  ssfzoulel  13800  seqf1olem1  14083  seqf1olem2  14084  hashge2el2difr  14521  hashtpg  14525  reusq0  15502  modfsummod  15831  incexclem  15873  sqrt2irr  16286  dvds2lem  16307  dvdslelem  16347  oddnn02np1  16386  divalglem8  16438  dfgcd2  16584  2mulprm  16731  ge2nprmge4  16739  euclemma  16751  iserodd  16874  ramcl  17068  setsstruct  17214  mreiincl  17640  joinfval  18419  meetfval  18433  dirge  18649  kerf1ghm  19266  sylow2alem1  19636  efgredlemb  19765  isdomn4  20717  rmodislmodlem  20928  lbspss  21082  lspsneu  21126  lspsnat  21148  lspsncv0  21149  opsrtoslem2  22081  distop  23003  epttop  23017  isclo2  23097  restdis  23187  subbascn  23263  cnrest2  23295  cnpresti  23297  isnrm2  23367  cmpsublem  23408  cmpcld  23411  dfconn2  23428  t1connperf  23445  1stcrest  23462  lly1stc  23505  uptx  23634  txcn  23635  prdstopn  23637  txconn  23698  cmphaushmeo  23809  fbasrn  23893  csdfil  23903  trufil  23919  fclscf  24034  alexsubALTlem3  24058  alexsubALT  24060  haustsms2  24146  ovoliunlem1  25538  ovoliunnul  25543  volsup2  25641  coeaddlem  26289  plymul0or  26323  radcnv0  26460  rtprmirr  26804  wilthlem3  27114  chtub  27257  gausslemma2dlem1a  27410  2sqlem10  27473  pntpbnd1  27631  sltval2  27702  noetalem1  27787  bday1s  27877  mptelee  28911  axeuclidlem  28978  axcontlem4  28983  elntg2  29001  uhgrissubgr  29293  finsumvtxdg2size  29569  wlkonl1iedg  29684  pthdivtx  29748  pthisspthorcycl  29823  wlkiswwlksupgr2  29898  eucrct2eupth  30265  isch3  31261  shmodsi  31409  orthin  31466  h1datomi  31601  stcltr2i  32295  atom1d  32373  sumdmdii  32435  cdj3lem1  32454  disjpreima  32598  lmxrge0  33952  dmvlsiga  34131  sibfof  34343  bnj600  34934  bnj1018g  34978  bnj1018  34979  bnj1173  35017  bnj1174  35018  subgrwlk  35138  cusgracyclt3v  35162  erdszelem9  35205  cvmlift2lem1  35308  satfvsucsuc  35371  sat1el2xp  35385  fmla0xp  35389  3jcadALT  35693  fundmpss  35768  outsideofrflx  36129  nn0prpwlem  36324  ivthALT  36337  fnessref  36359  neibastop2lem  36362  tailfb  36379  bj-axtd  36596  bj-nfimt  36640  bj-nfdt0  36697  bj-nnfand  36751  bj-sbievw2  36848  bj-2upleq  37014  bj-restn0  37092  icorempo  37353  isbasisrelowllem2  37358  rdgellim  37378  rdgssun  37380  pibt2  37419  wl-lem-moexsb  37570  matunitlindflem1  37624  poimirlem3  37631  poimirlem4  37632  poimirlem29  37657  mblfinlem3  37667  itg2addnclem3  37681  cover2  37723  fdc  37753  nninfnub  37759  equivtotbnd  37786  prdstotbnd  37802  cntotbnd  37804  ablo4pnp  37888  isdrngo3  37967  crngohomfo  38014  intidl  38037  or32dd  38102  iss2  38346  refressn  38445  eldisjlem19  38812  prtlem18  38879  prter2  38883  lsat0cv  39035  lfl1  39072  lkreqN  39172  atlrelat1  39323  pmaple  39764  pmapsub  39771  pclclN  39894  pclfinN  39903  osumcllem4N  39962  pexmidlem1N  39973  cdleme7ga  40251  lcfl7N  41504  eu6w  42691  dflim5  43347  omabs2  43350  ss2iundf  43677  brtrclfv2  43745  ismnushort  44325  nzss  44341  3impexpbicom  44505  alrim3con13v  44558  tratrb  44561  onfrALTlem3  44569  onfrALTlem2  44571  onfrALTlem1  44573  trsspwALT2  44844  trsspwALT3  44845  relpmin  44978  relpfrlem  44979  trfr  44984  or2expropbi  47051  afv2orxorb  47245  lswn0  47436  ich2exprop  47463  prproropf1olem4  47498  paireqne  47503  reupr  47514  lighneallem4b  47601  sbgoldbwt  47769  sbgoldbst  47770  sbgoldbalt  47773  isupwlkg  48058  2zrngamgm  48166  fldivexpfllog2  48491  line2ylem  48677  fdomne0  48764