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  1705  sbequ1  2283  dfmoeu  2560  2moswapv  2654  mopick2  2662  2moswap  2669  2eu6  2681  necon3d  2976  necon1d  2977  ralrimd  3267  spcimegf  3514  spcegf  3546  spcimedv  3549  spc2gv  3554  spc3gv  3558  rspcimedv  3567  2reu1  3844  sssn  4781  pwpw0  4830  ssiun  5004  ssiun2  5005  replem  5240  wefrc  5644  ssrel  5758  dmcosseq  5959  dmcosseqOLD  5960  relssres  6010  trin2  6116  ssrnres  6169  sossfld  6177  reuop  6296  frpoinsg  6346  tron  6385  ordtri3or  6395  oneqmini  6416  fnun  6654  f1oun  6845  brprcneu  6876  brprcneuALT  6877  ssimaex  6971  chfnrn  7049  dffo4  7104  dffo5  7105  tpres  7208  fvclss  7246  isomin  7346  isofrlem  7349  isoselem  7350  fnoprabg  7544  mpt3fvd  7689  tfisg  7866  nnsuc  7896  f1oweALT  7985  releldmdifi  8057  bropopvvv  8102  bropfvvvvlem  8103  frxp  8141  poxp  8143  fnse  8153  poseq  8178  mpoxopynvov0g  8235  issmo2  8361  smores  8364  smogt  8379  rdglim2  8444  onelfvnef1  8453  tz7.48lemOLD  8455  tz7.49  8459  swoer  8753  qsss  8800  domtriord  9146  findcard  9183  findcard2  9184  pssnn  9188  ssfiALT  9193  findcard3  9278  frfi  9280  dffi3  9427  supmo  9448  infmo  9493  inf3lem4  9636  frinsg  9759  carddom2  10062  fidomtri2  10079  pm54.43  10086  infpwfien  10145  alephordi  10157  cardaleph  10172  carduniima  10179  cardinfima  10180  alephval3  10193  dfac5lem4  10209  dfac5  10211  dfac2b  10213  kmlem2  10234  cflm  10331  cfslb2n  10350  cfsmolem  10352  isf32lem9  10443  axcc4  10521  domtriomlem  10524  zorn2lem4  10581  zorn2lem6  10583  fpwwe2lem10  10729  fpwwe2lem11  10730  inttsk  10863  inar1  10864  intgru  10903  ingru  10904  indpi  10996  nqpr  11103  ltaddpr  11123  ltexprlem1  11125  ltexprlem5  11129  reclem2pr  11137  reclem4pr  11139  negn0  11749  zmulcl  12749  uzm1  13003  uzwo  13042  xmullem2  13399  icoshft  13608  difreicc  13619  fzouzsplit  13833  ssfzoulel  13899  seqf1olem1  14188  seqf1olem2  14189  hashge2el2difr  14630  hashtpg  14634  reusq0  15638  modfsummod  15967  incexclem  16011  sqrt2irr  16423  dvds2lem  16444  dvdslelem  16485  oddnn02np1  16524  divalglem8  16576  dfgcd2  16725  2mulprm  16874  ge2nprmge4  16883  euclemma  16895  iserodd  17019  ramcl  17213  setsstruct  17360  mreiincl  17772  joinfval  18551  meetfval  18565  dirge  18783  chnccat  18806  kerf1ghm  19467  sylow2alem1  19837  efgredlemb  19966  crngrhmfo  20732  isdomn4  20973  isdrng5  21014  rmodislmodlem  21210  lbspss  21363  lspsneu  21407  lspsnat  21429  lspsncv0  21430  opsrtoslem2  22371  matunitlindflem1  23000  distop  23319  epttop  23333  isclo2  23412  restdis  23502  subbascn  23578  cnrest2  23610  cnpresti  23612  isnrm2  23682  cmpsublem  23723  cmpcld  23726  dfconn2  23743  t1connperf  23760  1stcrest  23777  lly1stc  23821  uptx  23950  txcn  23951  prdstopn  23953  txconn  24014  cmphaushmeo  24125  fbasrn  24209  csdfil  24219  trufil  24235  fclscf  24350  alexsubALTlem3  24374  alexsubALT  24376  haustsms2  24462  ovoliunlem1  25829  ovoliunnul  25834  volsup2  25932  coeaddlem  26574  plymul0or  26605  radcnv0  26749  rtprmirr  27094  wilthlem3  27403  chtub  27545  gausslemma2dlem1a  27698  2sqlem10  27761  pntpbnd1  27919  ltsval2  28019  noetalem1  28104  bday1  28206  mpteleeOLD  29479  axeuclidlem  29546  axcontlem4  29551  elntg2  29569  uhgrissubgr  29862  finsumvtxdg2size  30137  wlkonl1iedg  30250  subgrwlk  30275  pthdivtx  30318  pthisspthorcycl  30396  wlkiswwlksupgr2  30472  eucrct2eupth  30852  isch3  31849  shmodsi  31997  orthin  32054  h1datomi  32189  stcltr2i  32883  atom1d  32961  sumdmdii  33023  cdj3lem1  33042  disjpreima  33226  lmxrge0  34631  dmvlsiga  34808  sibfof  35019  bnj600  35596  bnj1018g  35640  bnj1018  35641  bnj1173  35679  bnj1174  35680  rmo6  35757  fnfvintima  35763  trssfir1om  35790  trssfir1omregs  35861  karddom  35886  kardsdom  35887  onvf1odlem2  35952  onvf1odlem4  35954  onprcf1acwevdlem1  35965  cusgracyclt3v  35998  erdszelem9  36051  ptpconn  36085  cvmlift2lem1  36154  satfvsucsuc  36217  sat1el2xp  36231  fmla0xp  36235  3jcadALT  36539  fundmpss  36625  outsideofrflx  36985  nn0prpwlem  37203  ivthALT  37216  fnessref  37238  neibastop2lem  37241  tailfb  37258  bj-axtd  37557  bj-nfimt  37615  bj-nfdt0  37690  bj-nnfand  37750  bj-sbievw2  37851  bj-2upleq  38018  bj-restn0  38104  icorempo  38368  isbasisrelowllem2  38373  rdgellim  38393  rdgssun  38395  pibt2  38434  wl-lem-moexsb  38594  poimirlem3  38635  poimirlem4  38636  poimirlem29  38661  mblfinlem3  38671  itg2addnclem3  38685  cover2  38743  fdc  38773  nninfnub  38779  equivtotbnd  38806  prdstotbnd  38822  cntotbnd  38824  ablo4pnp  38908  isdrngo3  38987  crngohomfo  39034  intidl  39057  or32dd  39120  iss2  39370  refressn  39559  eldisjlem19  39939  prtlem18  40028  prter2  40032  lsat0cv  40184  lfl1  40221  lkreqN  40321  atlrelat1  40472  pmapsub  40919  pclclN  41042  pclfinN  41051  osumcllem4N  41110  pexmidlem1N  41121  cdleme7ga  41399  lcfl7N  42652  eu6w  43781  dflim5  44425  omabs2  44428  ss2iundf  44753  brtrclfv2  44821  ismnushort  45379  nzss  45395  3impexpbicom  45557  alrim3con13v  45610  tratrb  45613  onfrALTlem3  45621  onfrALTlem2  45623  onfrALTlem1  45625  trsspwALT2  45895  trsspwALT3  45896  relpmin  46036  relpfrlem  46037  trfr  46046  or2expropbi  48198  afv2orxorb  48392  lswn0  48620  ich2exprop  48647  prproropf1olem4  48682  paireqne  48687  reupr  48698  lighneallem4b  48788  sbgoldbwt  48969  sbgoldbst  48970  sbgoldbalt  48973  cycldlenngric  49120  isupwlkg  49329  2zrngamgm  49436  fldivexpfllog2  49771  line2ylem  49957  fdomne0  50055