Theorem 3imtr4g 299

Description: More general version of 3imtr4i 295. 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 245	. 2 ⊢ (𝜑 → (𝜃 → 𝜒))
4		3imtr4g.3	. 2 ⊢ (𝜏 ↔ 𝜒)
5	3, 4	imbitrrdi 255	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:  3anim123d  1471  3orim123d  1472  sbi1  2107  moim  2569  mo3  2589  2euswapv  2655  2euswap  2670  exists2  2686  nelcon3d  3065  ral2imi  3101  ralimdv2  3171  reximdv2  3172  reximd2a  3272  moeq3  3669  rmoim  3697  2reuswap  3703  2reuswap2  3704  2rmoswap  3718  ssel  3902  ssrexf  3975  ssrmof  3976  ssralv  3977  ssrexv  3978  ss2abim  3985  ss2abdv  3990  rabss3d  4006  sscon  4079  ssdif  4080  ssrin  4138  unss1  4183  difin0ss  4320  r19.2z  4454  sspw  4567  uniss  4874  ssuni  4892  intssuni  4929  iinssiun  4964  iunss1  4965  iinss1  4966  ss2iun  4969  iunxdif3  5054  disjss2  5072  disjss1  5075  disjss3  5101  ssbrd  5147  poss  5560  pofun  5576  soss  5578  frss  5614  sess1  5615  sess2  5616  wess  5636  relss  5757  ssrel2  5760  ssrelrel  5771  relop  5827  dmss  5883  dmcosseq  5959  dmcosseqOLD  5960  funss  6558  fss  6726  fun  6744  brprcneu  6875  brprcneuALT  6876  f1eqcocnv  7309  isores3  7343  isomin  7345  isopolem  7353  isosolem  7355  isowe2  7358  ovmpos  7568  dfwe2  7788  epweon  7789  onint  7804  orduniorsuc  7841  trom  7886  finds  7908  finds2  7910  f1oweALT  7984  tposfn2  8265  tposfo2  8266  tposf1o2  8269  fprlem2  8319  smores  8360  tz7.48lemOLD  8451  tz7.48-3  8454  oaass  8569  brinxper  8747  iiner  8810  xpdom2  9091  ssenen  9170  pssnn  9184  hartogs  9538  card2on  9548  elhf4  9912  ackbij1  10315  cfub  10326  fin23lem27  10406  fin1a2lem11  10488  fin1a2lem13  10490  hsmexlem2  10505  zorn2lem4  10577  ondomon  10647  gchina  10784  intgru  10899  ingru  10900  addclprlem2  11102  psslinpr  11116  ltexprlem3  11123  ltexprlem4  11124  reclem2pr  11133  suplem1pr  11137  sup2  12273  nnind  12353  nnunb  12602  uzind  12791  xmullem2  13395  xrsupsslem  13437  xrinfmsslem  13438  seqof  14202  hashfacen  14599  sswrd  14667  wrdind  14871  wrd2ind  14872  pfxccatin12lem2  14880  cau3lem  15522  caubnd  15526  sumodd  16558  vdwnnlem2  17174  ramub2  17192  fthres2  18109  oduprs  18474  odupos  18500  chnrss  18789  chndss  18790  cycsubm  19417  lsmdisj2  19896  gsumxp2  20194  pgpfac1lem3  20293  nrhmzr  20789  subrgdvds  20838  isdrng5  21008  lspdisj  21403  lspprat  21431  lbsextlem2  21437  ocv2ss  21979  ocvin  21980  coe1fzgsumd  22622  evl1gsumd  22675  tgcl  23287  epttop  23327  cmpsub  23718  tgcmp  23719  hauscmplem  23724  dfconn2  23737  llyss  23798  nllyss  23799  locfincmp  23845  txcnpi  23927  txcnp  23939  snfil  24183  fgcl  24197  filconn  24202  filuni  24204  cfinfil  24212  csdfil  24213  supfil  24214  ufildom1  24245  fin1aufil  24251  fmfnfmlem3  24275  ptcmplem2  24372  cldsubg  24430  iscau3  25599  iscau4  25600  caussi  25618  volfiniun  25868  plycj  26596  abelth  26768  wilthlem2  27396  lgsdir2lem4  27655  gausslemma2dlem0i  27691  gausslemma2dlem1a  27692  pntleml  27938  nna4b4nsq  27990  ltsres  28019  nosupno  28060  noinfno  28075  noseqinds  28679  plngrotlem2  29266  uhgr0vsize0  29820  cusgrfilem2  30037  uhgrvd00  30115  subgrtrl  30294  subgrpth  30356  subgrcycl  30385  clwwisshclwws  30606  frcond3  30870  frgrncvvdeqlem2  30901  lpni  31082  ubthlem1  31472  chintcli  31933  h1de2i  32155  spansnm0i  32252  strlem1  32852  mdslmd1i  32931  reuxfrdf  33087  n0nsnel  33111  disjss1f  33166  disjpreima  33178  ssrelf  33209  suppss3  33315  nnindf  33411  wrdt2ind  33516  crefss  34481  esumpcvgval  34710  cbvex1v  35704  r1filim  35729  onvf1odlem4  35885  derangenlem  35936  connpconn  36000  cvmsss2  36039  pocnv  36528  wzel  36586  in-ax8  37013  naim1  37177  naim2  37178  waj-ax  37202  lukshef-ax2  37203  ttctr  37281  dfttc2g  37294  bj-exim  37509  bj-sbievw1  37757  wl-dfcleq  38438  poimirlem26  38565  poimirlem30  38569  poimirlem32  38571  itg2addnclem  38590  ismtybndlem  38741  ablo4pnp  38815  isdrngo3  38894  keridl  38967  ispridl2  38973  ispridlc  39005  trcoss  39505  funALTVss  39717  disjss  39764  eldisjss  39771  prter1  39937  lshpdisj  40045  snatpsubN  40808  pmapglb2N  40829  pmapglb2xN  40830  elpaddn0  40858  sn-sup2  43556  mzpindd  43757  pellexlem3  43838  pellexlem5  43840  pellex  43842  2nn0ind  43952  lnr2i  44118  ofoaid1  44360  ofoaid2  44361  intabssd  44520  iunrelexpuztr  44719  hess  44780  frege52aid  44858  frege52b  44889  neik0pk1imk0  45047  relpmin  45942  rankrelp  45950  n0nsn2el  48095  imasetpreimafvbijlemfv1  48485  isubgredg  48964  stgrusgra  49057  isubgr3stgrlem6  49069  iinfsubc  50166  elsetrecslem  50792