Theorem 3imtr4g 296

Description: More general version of 3imtr4i 292. Useful for converting definitions in a formula. (Contributed by NM, 20-May-1996.) (Proof shortened by Wolf Lammen, 20-Dec-2013.)

Hypotheses

Ref	Expression
3imtr4g.1	⊢ (𝜑 → (𝜓 → 𝜒))
3imtr4g.2	⊢ (𝜃 ↔ 𝜓)
3imtr4g.3	⊢ (𝜏 ↔ 𝜒)

Assertion

Ref	Expression
3imtr4g	⊢ (𝜑 → (𝜃 → 𝜏))

Proof of Theorem 3imtr4g

Step	Hyp	Ref	Expression
1		3imtr4g.2	. . 3 ⊢ (𝜃 ↔ 𝜓)
2		3imtr4g.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	biimtrid 242	. 2 ⊢ (𝜑 → (𝜃 → 𝜒))
4		3imtr4g.3	. 2 ⊢ (𝜏 ↔ 𝜒)
5	3, 4	imbitrrdi 252	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:  3anim123d  1446  3orim123d  1447  sbi1  2077  moim  2545  mo3  2565  2euswapv  2631  2euswap  2646  exists2  2663  nelcon3d  3041  ral2imi  3076  ralimdv2  3146  reximdv2  3147  reximd2a  3247  moeq3  3671  rmoim  3699  2reuswap  3705  2reuswap2  3706  2rmoswap  3720  ssel  3928  sstr2OLD  3942  ssrexf  4001  ssrmof  4002  ssralv  4003  ssrexv  4004  ss2abim  4013  ss2abdv  4018  rabss3d  4034  sscon  4096  ssdif  4097  unss1  4138  ssrin  4195  difin0ss  4326  r19.2z  4453  sspw  4566  uniss  4872  ssuni  4889  intssuni  4926  iinssiun  4961  iunss1  4962  iinss1  4963  ss2iun  4966  iunxdif3  5051  disjss2  5069  disjss1  5072  disjss3  5098  ssbrd  5142  poss  5535  pofun  5551  soss  5553  frss  5589  sess1  5590  sess2  5591  wess  5611  relss  5732  ssrel2  5735  ssrelrel  5746  relop  5800  dmss  5852  dmcosseq  5928  dmcosseqOLD  5929  dmcosseqOLDOLD  5930  funss  6512  f1imadifssran  6579  fss  6679  fun  6697  brprcneu  6825  brprcneuALT  6826  f1eqcocnv  7249  isores3  7283  isomin  7285  isopolem  7293  isosolem  7295  isowe2  7298  ovmpos  7508  dfwe2  7721  epweon  7722  onint  7737  orduniorsuc  7774  trom  7819  finds  7840  finds2  7842  f1oweALT  7918  tposfn2  8192  tposfo2  8193  tposf1o2  8196  fprlem2  8245  smores  8286  tz7.48lem  8374  tz7.48-3  8377  oaass  8490  brinxper  8667  iiner  8730  xpdom2  9004  ssenen  9083  pssnn  9097  hartogs  9453  card2on  9463  ackbij1  10151  cfub  10163  fin23lem27  10242  fin1a2lem11  10324  fin1a2lem13  10326  hsmexlem2  10341  zorn2lem4  10413  ondomon  10477  gchina  10614  intgru  10729  ingru  10730  addclprlem2  10932  psslinpr  10946  ltexprlem3  10953  ltexprlem4  10954  reclem2pr  10963  suplem1pr  10967  sup2  12102  nnind  12167  nnunb  12401  uzind  12588  xmullem2  13184  xrsupsslem  13226  xrinfmsslem  13227  seqof  13986  hashfacen  14381  sswrd  14449  wrdind  14649  wrd2ind  14650  pfxccatin12lem2  14658  cau3lem  15282  caubnd  15286  sumodd  16319  vdwnnlem2  16928  ramub2  16946  fthres2  17862  oduprs  18227  odupos  18253  chnrss  18542  chndss  18543  cycsubm  19135  lsmdisj2  19615  gsumxp2  19913  pgpfac1lem3  20012  nrhmzr  20474  subrgdvds  20523  lspdisj  21084  lspprat  21112  lbsextlem2  21118  ocv2ss  21632  ocvin  21633  coe1fzgsumd  22252  evl1gsumd  22305  tgcl  22917  epttop  22957  cmpsub  23348  tgcmp  23349  hauscmplem  23354  dfconn2  23367  llyss  23427  nllyss  23428  locfincmp  23474  txcnpi  23556  txcnp  23568  snfil  23812  fgcl  23826  filconn  23831  filuni  23833  cfinfil  23841  csdfil  23842  supfil  23843  ufildom1  23874  fin1aufil  23880  fmfnfmlem3  23904  ptcmplem2  24001  cldsubg  24059  iscau3  25238  iscau4  25239  caussi  25257  volfiniun  25508  plycj  26243  plycjOLD  26245  abelth  26411  wilthlem2  27039  lgsdir2lem4  27299  gausslemma2dlem0i  27335  gausslemma2dlem1a  27336  pntleml  27582  ltsres  27634  nosupno  27675  noinfno  27690  noseqinds  28293  uhgr0vsize0  29316  cusgrfilem2  29534  uhgrvd00  29612  clwwisshclwws  30094  frcond3  30348  frgrncvvdeqlem2  30379  lpni  30559  ubthlem1  30949  chintcli  31410  h1de2i  31632  spansnm0i  31729  strlem1  32329  mdslmd1i  32408  reuxfrdf  32568  n0nsnel  32593  disjss1f  32650  disjpreima  32662  ssrelf  32696  suppss3  32804  nnindf  32902  wrdt2ind  33037  crefss  34008  esumpcvgval  34237  cbvex1v  35232  r1filim  35262  onvf1odlem4  35302  subgrtrl  35329  subgrpth  35330  subgrcycl  35331  derangenlem  35367  connpconn  35431  cvmsss2  35470  pocnv  35959  wzel  36018  in-ax8  36420  naim1  36585  naim2  36586  waj-ax  36610  lukshef-ax2  36611  bj-eximALT  36843  bj-sbievw1  37048  poimirlem26  37849  poimirlem30  37853  poimirlem32  37855  itg2addnclem  37874  ismtybndlem  38009  ablo4pnp  38083  isdrngo3  38162  keridl  38235  ispridl2  38241  ispridlc  38273  trcoss  38775  funALTVss  38987  disjss  39034  eldisjss  39041  prter1  39207  lshpdisj  39315  snatpsubN  40078  pmapglb2N  40099  pmapglb2xN  40100  elpaddn0  40128  sn-sup2  42813  nna4b4nsq  42970  mzpindd  43055  pellexlem3  43140  pellexlem5  43142  pellex  43144  2nn0ind  43254  lnr2i  43425  ofoaid1  43667  ofoaid2  43668  intabssd  43827  iunrelexpuztr  44027  hess  44088  frege52aid  44166  frege52b  44197  neik0pk1imk0  44355  relpmin  45260  rankrelp  45268  n0nsn2el  47338  imasetpreimafvbijlemfv1  47716  isubgredg  48179  stgrusgra  48272  isubgr3stgrlem6  48284  iinfsubc  49370  elsetrecslem  50011