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  2255  dfmoeu  2535  2moswapv  2629  mopick2  2637  2moswap  2644  2eu6  2657  necon3d  2953  necon1d  2954  ralrimd  3241  spcimegf  3508  spcegf  3546  spcimedv  3549  spc2gv  3554  spc3gv  3558  rspcimedv  3567  2reu1  3847  pwpw0  4769  sssn  4782  ssiun  5002  ssiun2  5003  wefrc  5618  ssrel  5732  dmcosseq  5927  dmcosseqOLD  5928  dmcosseqOLDOLD  5929  relssres  5981  trin2  6080  ssrnres  6136  sossfld  6144  reuop  6251  frpoinsg  6301  tron  6340  ordtri3or  6349  oneqmini  6370  fnun  6606  f1oun  6793  brprcneu  6824  brprcneuALT  6825  ssimaex  6919  chfnrn  6994  dffo4  7048  dffo5  7049  tpres  7147  fvclss  7187  isomin  7283  isofrlem  7286  isoselem  7287  fnoprabg  7481  tfisg  7796  nnsuc  7826  f1oweALT  7916  releldmdifi  7989  bropopvvv  8032  bropfvvvvlem  8033  frxp  8068  poxp  8070  fnse  8075  poseq  8100  mpoxopynvov0g  8156  issmo2  8281  smores  8284  smogt  8299  rdglim2  8363  tz7.48lem  8372  tz7.49  8376  swoer  8666  qsss  8713  domtriord  9051  findcard  9088  findcard2  9089  pssnn  9093  ssfiALT  9098  findcard3  9183  frfi  9185  dffi3  9334  supmo  9355  infmo  9400  inf3lem4  9540  frinsg  9663  carddom2  9889  fidomtri2  9906  pm54.43  9913  infpwfien  9972  alephordi  9984  cardaleph  9999  carduniima  10006  cardinfima  10007  alephval3  10020  dfac5lem4  10036  dfac5lem4OLD  10038  dfac5  10039  dfac2b  10041  kmlem2  10062  cflm  10160  cfslb2n  10178  cfsmolem  10180  isf32lem9  10271  axcc4  10349  domtriomlem  10352  zorn2lem4  10409  zorn2lem6  10411  fpwwe2lem10  10551  fpwwe2lem11  10552  inttsk  10685  inar1  10686  intgru  10725  ingru  10726  indpi  10818  nqpr  10925  ltaddpr  10945  ltexprlem1  10947  ltexprlem5  10951  reclem2pr  10959  reclem4pr  10961  negn0  11566  zmulcl  12540  uzm1  12785  uzwo  12824  xmullem2  13180  icoshft  13389  difreicc  13400  fzouzsplit  13610  ssfzoulel  13676  seqf1olem1  13964  seqf1olem2  13965  hashge2el2difr  14404  hashtpg  14408  reusq0  15388  modfsummod  15717  incexclem  15759  sqrt2irr  16174  dvds2lem  16195  dvdslelem  16236  oddnn02np1  16275  divalglem8  16327  dfgcd2  16473  2mulprm  16620  ge2nprmge4  16628  euclemma  16640  iserodd  16763  ramcl  16957  setsstruct  17103  mreiincl  17515  joinfval  18294  meetfval  18308  dirge  18526  chnccat  18549  kerf1ghm  19176  sylow2alem1  19546  efgredlemb  19675  isdomn4  20649  rmodislmodlem  20880  lbspss  21034  lspsneu  21078  lspsnat  21100  lspsncv0  21101  opsrtoslem2  22011  distop  22939  epttop  22953  isclo2  23032  restdis  23122  subbascn  23198  cnrest2  23230  cnpresti  23232  isnrm2  23302  cmpsublem  23343  cmpcld  23346  dfconn2  23363  t1connperf  23380  1stcrest  23397  lly1stc  23440  uptx  23569  txcn  23570  prdstopn  23572  txconn  23633  cmphaushmeo  23744  fbasrn  23828  csdfil  23838  trufil  23854  fclscf  23969  alexsubALTlem3  23993  alexsubALT  23995  haustsms2  24081  ovoliunlem1  25459  ovoliunnul  25464  volsup2  25562  coeaddlem  26210  plymul0or  26244  radcnv0  26381  rtprmirr  26726  wilthlem3  27036  chtub  27179  gausslemma2dlem1a  27332  2sqlem10  27395  pntpbnd1  27553  ltsval2  27624  noetalem1  27709  bday1  27810  mpteleeOLD  28968  axeuclidlem  29035  axcontlem4  29040  elntg2  29058  uhgrissubgr  29348  finsumvtxdg2size  29624  wlkonl1iedg  29737  pthdivtx  29800  pthisspthorcycl  29875  wlkiswwlksupgr2  29950  eucrct2eupth  30320  isch3  31316  shmodsi  31464  orthin  31521  h1datomi  31656  stcltr2i  32350  atom1d  32428  sumdmdii  32490  cdj3lem1  32509  disjpreima  32659  lmxrge0  34109  dmvlsiga  34286  sibfof  34497  bnj600  35075  bnj1018g  35119  bnj1018  35120  bnj1173  35158  bnj1174  35159  trssfir1om  35267  trssfir1omregs  35292  onvf1odlem2  35298  onvf1odlem4  35300  subgrwlk  35326  cusgracyclt3v  35350  erdszelem9  35393  cvmlift2lem1  35496  satfvsucsuc  35559  sat1el2xp  35573  fmla0xp  35577  3jcadALT  35881  fundmpss  35961  outsideofrflx  36321  nn0prpwlem  36516  ivthALT  36529  fnessref  36551  neibastop2lem  36554  tailfb  36571  bj-axtd  36794  bj-nfimt  36838  bj-nfdt0  36896  bj-nnfand  36950  bj-sbievw2  37047  bj-2upleq  37213  bj-restn0  37291  icorempo  37552  isbasisrelowllem2  37557  rdgellim  37577  rdgssun  37579  pibt2  37618  wl-lem-moexsb  37769  matunitlindflem1  37813  poimirlem3  37820  poimirlem4  37821  poimirlem29  37846  mblfinlem3  37856  itg2addnclem3  37870  cover2  37912  fdc  37942  nninfnub  37948  equivtotbnd  37975  prdstotbnd  37991  cntotbnd  37993  ablo4pnp  38077  isdrngo3  38156  crngohomfo  38203  intidl  38226  or32dd  38291  iss2  38533  refressn  38702  eldisjlem19  39065  prtlem18  39133  prter2  39137  lsat0cv  39289  lfl1  39326  lkreqN  39426  atlrelat1  39577  pmapsub  40024  pclclN  40147  pclfinN  40156  osumcllem4N  40215  pexmidlem1N  40226  cdleme7ga  40504  lcfl7N  41757  eu6w  42915  dflim5  43567  omabs2  43570  ss2iundf  43896  brtrclfv2  43964  ismnushort  44538  nzss  44554  3impexpbicom  44717  alrim3con13v  44770  tratrb  44773  onfrALTlem3  44781  onfrALTlem2  44783  onfrALTlem1  44785  trsspwALT2  45055  trsspwALT3  45056  relpmin  45189  relpfrlem  45190  trfr  45199  or2expropbi  47276  afv2orxorb  47470  lswn0  47686  ich2exprop  47713  prproropf1olem4  47748  paireqne  47753  reupr  47764  lighneallem4b  47851  sbgoldbwt  48019  sbgoldbst  48020  sbgoldbalt  48023  cycldlenngric  48170  isupwlkg  48379  2zrngamgm  48487  fldivexpfllog2  48807  line2ylem  48993  fdomne0  49091