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  1670  sbequ1  2246  dfmoeu  2534  2moswapv  2627  mopick2  2635  2moswap  2642  2eu6  2655  necon3d  2959  necon1d  2960  ralrimd  3262  spcimegf  3551  spcegf  3592  spcimedv  3595  spc2gv  3600  spc3gv  3604  rspcimedv  3613  2reu1  3906  pwpw0  4818  sssn  4831  ssiun  5051  ssiun2  5052  wefrc  5683  ssrel  5795  ssrelOLD  5796  dmcosseq  5990  dmcosseqOLD  5991  relssres  6042  trin2  6146  ssrnres  6200  sossfld  6208  reuop  6315  frpoinsg  6366  wfisgOLD  6377  tron  6409  ordtri3or  6418  oneqmini  6438  fnun  6683  f1oun  6868  brprcneu  6897  brprcneuALT  6898  ssimaex  6994  chfnrn  7069  dffo4  7123  dffo5  7124  tpres  7221  fvclss  7261  isomin  7357  isofrlem  7360  isoselem  7361  fnoprabg  7556  tfisg  7875  nnsuc  7905  f1oweALT  7996  releldmdifi  8069  bropopvvv  8114  bropfvvvvlem  8115  frxp  8150  poxp  8152  fnse  8157  poseq  8182  mpoxopynvov0g  8238  issmo2  8388  smores  8391  smogt  8406  rdglim2  8471  tz7.48lem  8480  tz7.49  8484  swoer  8775  qsss  8817  domtriord  9162  findcard  9202  findcard2  9203  pssnn  9207  ssfiALT  9213  findcard3  9316  findcard3OLD  9317  frfi  9319  dffi3  9469  supmo  9490  infmo  9533  inf3lem4  9669  frinsg  9789  carddom2  10015  fidomtri2  10032  pm54.43  10039  infpwfien  10100  alephordi  10112  cardaleph  10127  carduniima  10134  cardinfima  10135  alephval3  10148  dfac5lem4  10164  dfac5lem4OLD  10166  dfac5  10167  dfac2b  10169  kmlem2  10190  cflm  10288  cfslb2n  10306  cfsmolem  10308  isf32lem9  10399  axcc4  10477  domtriomlem  10480  zorn2lem4  10537  zorn2lem6  10539  fpwwe2lem10  10678  fpwwe2lem11  10679  inttsk  10812  inar1  10813  intgru  10852  ingru  10853  indpi  10945  nqpr  11052  ltaddpr  11072  ltexprlem1  11074  ltexprlem5  11078  reclem2pr  11086  reclem4pr  11088  negn0  11690  zmulcl  12664  uzm1  12914  uzwo  12951  xmullem2  13304  icoshft  13510  difreicc  13521  fzouzsplit  13731  ssfzoulel  13796  seqf1olem1  14079  seqf1olem2  14080  hashge2el2difr  14517  hashtpg  14521  reusq0  15498  modfsummod  15827  incexclem  15869  sqrt2irr  16282  dvds2lem  16303  dvdslelem  16343  oddnn02np1  16382  divalglem8  16434  dfgcd2  16580  2mulprm  16727  ge2nprmge4  16735  euclemma  16747  iserodd  16869  ramcl  17063  setsstruct  17210  mreiincl  17641  joinfval  18431  meetfval  18445  dirge  18661  kerf1ghm  19278  sylow2alem1  19650  efgredlemb  19779  isdomn4  20733  rmodislmodlem  20944  lbspss  21099  lspsneu  21143  lspsnat  21165  lspsncv0  21166  opsrtoslem2  22098  distop  23018  epttop  23032  isclo2  23112  restdis  23202  subbascn  23278  cnrest2  23310  cnpresti  23312  isnrm2  23382  cmpsublem  23423  cmpcld  23426  dfconn2  23443  t1connperf  23460  1stcrest  23477  lly1stc  23520  uptx  23649  txcn  23650  prdstopn  23652  txconn  23713  cmphaushmeo  23824  fbasrn  23908  csdfil  23918  trufil  23934  fclscf  24049  alexsubALTlem3  24073  alexsubALT  24075  haustsms2  24161  ovoliunlem1  25551  ovoliunnul  25556  volsup2  25654  coeaddlem  26303  plymul0or  26337  radcnv0  26474  rtprmirr  26818  wilthlem3  27128  chtub  27271  gausslemma2dlem1a  27424  2sqlem10  27487  pntpbnd1  27645  sltval2  27716  noetalem1  27801  bday1s  27891  mptelee  28925  axeuclidlem  28992  axcontlem4  28997  elntg2  29015  uhgrissubgr  29307  finsumvtxdg2size  29583  wlkonl1iedg  29698  pthdivtx  29762  wlkiswwlksupgr2  29907  eucrct2eupth  30274  isch3  31270  shmodsi  31418  orthin  31475  h1datomi  31610  stcltr2i  32304  atom1d  32382  sumdmdii  32444  cdj3lem1  32463  disjpreima  32604  lmxrge0  33913  dmvlsiga  34110  sibfof  34322  bnj600  34912  bnj1018g  34956  bnj1018  34957  bnj1173  34995  bnj1174  34996  pthisspthorcycl  35113  subgrwlk  35117  cusgracyclt3v  35141  erdszelem9  35184  cvmlift2lem1  35287  satfvsucsuc  35350  sat1el2xp  35364  fmla0xp  35368  3jcadALT  35672  fundmpss  35748  outsideofrflx  36109  nn0prpwlem  36305  ivthALT  36318  fnessref  36340  neibastop2lem  36343  tailfb  36360  bj-axtd  36577  bj-nfimt  36621  bj-nfdt0  36678  bj-nnfand  36732  bj-sbievw2  36829  bj-2upleq  36995  bj-restn0  37073  icorempo  37334  isbasisrelowllem2  37339  rdgellim  37359  rdgssun  37361  pibt2  37400  wl-lem-moexsb  37549  matunitlindflem1  37603  poimirlem3  37610  poimirlem4  37611  poimirlem29  37636  mblfinlem3  37646  itg2addnclem3  37660  cover2  37702  fdc  37732  nninfnub  37738  equivtotbnd  37765  prdstotbnd  37781  cntotbnd  37783  ablo4pnp  37867  isdrngo3  37946  crngohomfo  37993  intidl  38016  or32dd  38081  iss2  38326  refressn  38425  eldisjlem19  38792  prtlem18  38859  prter2  38863  lsat0cv  39015  lfl1  39052  lkreqN  39152  atlrelat1  39303  pmaple  39744  pmapsub  39751  pclclN  39874  pclfinN  39883  osumcllem4N  39942  pexmidlem1N  39953  cdleme7ga  40231  lcfl7N  41484  eu6w  42663  dflim5  43319  omabs2  43322  ss2iundf  43649  brtrclfv2  43717  ismnushort  44297  nzss  44313  3impexpbicom  44477  alrim3con13v  44531  tratrb  44534  onfrALTlem3  44542  onfrALTlem2  44544  onfrALTlem1  44546  trsspwALT2  44817  trsspwALT3  44818  or2expropbi  46984  afv2orxorb  47178  lswn0  47369  ich2exprop  47396  prproropf1olem4  47431  paireqne  47436  reupr  47447  lighneallem4b  47534  sbgoldbwt  47702  sbgoldbst  47703  sbgoldbalt  47706  isupwlkg  47981  2zrngamgm  48089  fldivexpfllog2  48415  line2ylem  48601  fdomne0  48680