Theorem imbitrrdi 255

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  3imtr4g  299  nic-ax  1706  sbequ1  2287  dfmoeu  2566  2moswapv  2660  mopick2  2668  2moswap  2675  2eu6  2687  necon3d  2982  necon1d  2983  ralrimd  3273  spcimegf  3522  spcegf  3554  spcimedv  3557  spc2gv  3562  spc3gv  3566  rspcimedv  3575  2reu1  3854  pwpw0  4784  sssn  4797  ssiun  5016  ssiun2  5017  replem  5254  wefrc  5660  ssrel  5774  dmcosseq  5973  dmcosseqOLD  5974  relssres  6026  trin2  6128  ssrnres  6181  sossfld  6189  reuop  6301  frpoinsg  6351  tron  6390  ordtri3or  6400  oneqmini  6421  fnun  6656  f1oun  6847  brprcneu  6878  brprcneuALT  6879  ssimaex  6973  chfnrn  7051  dffo4  7105  dffo5  7106  tpres  7206  fvclss  7246  isomin  7346  isofrlem  7349  isoselem  7350  fnoprabg  7546  tfisg  7859  nnsuc  7889  f1oweALT  7978  releldmdifi  8051  bropopvvv  8094  bropfvvvvlem  8095  frxp  8131  poxp  8133  fnse  8138  poseq  8163  mpoxopynvov0g  8219  issmo2  8345  smores  8348  smogt  8363  rdglim2  8428  tz7.48lem  8437  tz7.49  8441  swoer  8735  qsss  8782  domtriord  9121  findcard  9158  findcard2  9159  pssnn  9163  ssfiALT  9168  findcard3  9253  frfi  9255  dffi3  9401  supmo  9422  infmo  9467  inf3lem4  9610  frinsg  9733  carddom2  9982  fidomtri2  9999  pm54.43  10006  infpwfien  10065  alephordi  10077  cardaleph  10092  carduniima  10099  cardinfima  10100  alephval3  10113  dfac5lem4  10129  dfac5  10131  dfac2b  10133  kmlem2  10154  cflm  10251  cfslb2n  10270  cfsmolem  10272  isf32lem9  10363  axcc4  10441  domtriomlem  10444  zorn2lem4  10501  zorn2lem6  10503  fpwwe2lem10  10643  fpwwe2lem11  10644  inttsk  10777  inar1  10778  intgru  10817  ingru  10818  indpi  10910  nqpr  11017  ltaddpr  11037  ltexprlem1  11039  ltexprlem5  11043  reclem2pr  11051  reclem4pr  11053  negn0  11661  zmulcl  12661  uzm1  12914  uzwo  12953  xmullem2  13309  icoshft  13518  difreicc  13529  fzouzsplit  13742  ssfzoulel  13808  seqf1olem1  14097  seqf1olem2  14098  hashge2el2difr  14538  hashtpg  14542  reusq0  15542  modfsummod  15872  incexclem  15916  sqrt2irr  16330  dvds2lem  16351  dvdslelem  16392  oddnn02np1  16431  divalglem8  16483  dfgcd2  16629  2mulprm  16776  ge2nprmge4  16785  euclemma  16797  iserodd  16920  ramcl  17114  setsstruct  17261  mreiincl  17673  joinfval  18452  meetfval  18466  dirge  18684  chnccat  18707  kerf1ghm  19348  sylow2alem1  19718  efgredlemb  19847  crngrhmfo  20611  isdomn4  20851  isdrng5  20891  rmodislmodlem  21087  lbspss  21240  lspsneu  21284  lspsnat  21306  lspsncv0  21307  opsrtoslem2  22244  distop  23189  epttop  23203  isclo2  23282  restdis  23372  subbascn  23448  cnrest2  23480  cnpresti  23482  isnrm2  23552  cmpsublem  23593  cmpcld  23596  dfconn2  23613  t1connperf  23630  1stcrest  23647  lly1stc  23690  uptx  23819  txcn  23820  prdstopn  23822  txconn  23883  cmphaushmeo  23994  fbasrn  24078  csdfil  24088  trufil  24104  fclscf  24219  alexsubALTlem3  24243  alexsubALT  24245  haustsms2  24331  ovoliunlem1  25698  ovoliunnul  25703  volsup2  25801  coeaddlem  26443  plymul0or  26476  radcnv0  26616  rtprmirr  26962  wilthlem3  27271  chtub  27413  gausslemma2dlem1a  27566  2sqlem10  27629  pntpbnd1  27787  ltsval2  27857  noetalem1  27942  bday1  28044  mpteleeOLD  29282  axeuclidlem  29349  axcontlem4  29354  elntg2  29372  uhgrissubgr  29662  finsumvtxdg2size  29937  wlkonl1iedg  30050  pthdivtx  30113  pthisspthorcycl  30188  wlkiswwlksupgr2  30263  eucrct2eupth  30633  isch3  31630  shmodsi  31778  orthin  31835  h1datomi  31970  stcltr2i  32664  atom1d  32742  sumdmdii  32804  cdj3lem1  32823  disjpreima  32966  lmxrge0  34373  dmvlsiga  34550  sibfof  34762  bnj600  35339  bnj1018g  35383  bnj1018  35384  bnj1173  35422  bnj1174  35423  fnfvintima  35502  trssfir1om  35532  trssfir1omregs  35573  karddom  35598  kardsdom  35599  onvf1odlem2  35612  onvf1odlem4  35614  subgrwlk  35645  cusgracyclt3v  35669  erdszelem9  35712  cvmlift2lem1  35815  satfvsucsuc  35878  sat1el2xp  35892  fmla0xp  35896  3jcadALT  36200  fundmpss  36280  outsideofrflx  36640  nn0prpwlem  36874  ivthALT  36887  fnessref  36909  neibastop2lem  36912  tailfb  36929  mh-inf3f1  37093  bj-axtd  37228  bj-nfimt  37286  bj-nfdt0  37361  bj-nnfand  37421  bj-sbievw2  37522  bj-2upleq  37689  bj-restn0  37773  icorempo  38038  isbasisrelowllem2  38043  rdgellim  38063  rdgssun  38065  pibt2  38104  wl-lem-moexsb  38264  matunitlindflem1  38308  poimirlem3  38315  poimirlem4  38316  poimirlem29  38341  mblfinlem3  38351  itg2addnclem3  38365  cover2  38407  fdc  38437  nninfnub  38443  equivtotbnd  38470  prdstotbnd  38486  cntotbnd  38488  ablo4pnp  38572  isdrngo3  38651  crngohomfo  38698  intidl  38721  or32dd  38784  iss2  39034  refressn  39223  eldisjlem19  39603  prtlem18  39692  prter2  39696  lsat0cv  39848  lfl1  39885  lkreqN  39985  atlrelat1  40136  pmapsub  40583  pclclN  40706  pclfinN  40715  osumcllem4N  40774  pexmidlem1N  40785  cdleme7ga  41063  lcfl7N  42316  eu6w  43449  dflim5  44097  omabs2  44100  ss2iundf  44426  brtrclfv2  44494  ismnushort  45052  nzss  45068  3impexpbicom  45230  alrim3con13v  45283  tratrb  45286  onfrALTlem3  45294  onfrALTlem2  45296  onfrALTlem1  45298  trsspwALT2  45568  trsspwALT3  45569  relpmin  45702  relpfrlem  45703  trfr  45712  or2expropbi  47812  afv2orxorb  48006  lswn0  48234  ich2exprop  48261  prproropf1olem4  48296  paireqne  48301  reupr  48312  lighneallem4b  48402  sbgoldbwt  48583  sbgoldbst  48584  sbgoldbalt  48587  cycldlenngric  48734  isupwlkg  48943  2zrngamgm  49051  fldivexpfllog2  49386  line2ylem  49572  fdomne0  49669