Theorem 3imtr4g 556

Description: More general version of 3imtr4i 217. Useful for converting definitions in a formula.

Hypotheses

Ref	Expression
3imtr4g.1	⊢ (φ → (ψ → χ))
3imtr4g.2	⊢ (θ ↔ ψ)
3imtr4g.3	⊢ (τ ↔ χ)

Assertion

Ref	Expression
3imtr4g	⊢ (φ → (θ → τ))

Proof of Theorem 3imtr4g

Step	Hyp	Ref	Expression
1		3imtr4g.1	. 2 ⊢ (φ → (ψ → χ))
2		3imtr4g.2	. . 3 ⊢ (θ ↔ ψ)
3	2	bicomi 170	. 2 ⊢ (ψ ↔ θ)
4		3imtr4g.3	. . 3 ⊢ (τ ↔ χ)
5	4	bicomi 170	. 2 ⊢ (χ ↔ τ)
6	1, 3, 5	3imtr3g 555	1 ⊢ (φ → (θ → τ))

Syntax hints:   → wi 3   ↔ wb 144

This theorem is referenced by:  pm3.48 560  pm5.74 586  ordi 599  3anim123d 906  3orim123d 907  19.22 1075  hbbid 1148  a12stdy1 1411  a12studyALT 1418  immo 1456  moimv 1458  2euswap 1485  hbabd 1510  r19.20 1748  r19.20da 1754  r19.20dv2 1757  r19.22dv2 1782  moeq3 1967  2reuswap 1983  hbcsb1g 2075  hbcsbg 2077  ssel 2115  sstr2 2123  sscon 2223  ssdif 2224  unss1 2251  ssrin 2286  difin0ss 2385  r19.2z 2401  prel12 2549  ssuni 2589  intss 2621  intssuni 2622  ss2iun 2645  iununi 2686  ssbrd 2729  sspwb 2835  poss 2919  soss 2931  frss 2951  wess 2963  dfwe2 3140  onint 3152  orduniorsuc 3184  finds 3244  finds2 3246  relss 3333  ssxp 3345  relop 3365  cnvss 3381  dmss 3401  dffun8 3645  fun 3748  isomin 4013  f1oweALT 4020  tz7.48lem 4256  tz7.48-3 4259  oaass 4331  ss2ixp 4495  xpdom2 4583  ensdomtr 4616  domsdomtr 4621  mapenlem2 4637  mapdom2 4641  ssenen 4651  pssnn 4681  r1pwcl 4833  zorn2lem4 4937  zorn2lem7 4940  ondomon 5006  cfub 5058  1pr 5271  addclprlem2 5273  distrlem1pr 5281  psslinpr 5289  ltexprlem3 5298  ltexprlem4 5299  reclem2pr 5311  suplem1pr 5315  suppsr2 5377  suppsr3 5378  axrrecex 5438  ltmullem 5794  prodge0i 5960  nnind 6082  sup2 6219  nnunb 6238  xrsupsslem 6244  xrinfmsslem 6245  supxrre 6251  uzind 6376  elioc2 6516  elico2 6517  elicc2 6518  caucvglem4 7363  efseq0ex 7516  infdif2 7781  tgcl 7836  ubthlem6 8792  chsscmi 9388  occon 9436  chintcli 9571  shlessi 9623  h1de2i 9752  spansnm0i 9873  strlem1 10458  mdslmd1i 10537  uninqs 10730  eqindhome 11047  qusp 11068  lpni 11417  fictb 11423  ordtypelem4 11430  hartog 11436  compcov 11486  compsub 11488  alexsublem3 11498  cnconn 11503  isfne3 11543  topbasfne 11560  fnessref 11564  neibastop1 11579  neibastop2 11584  fbssint 11626  ufileu 11658  ufinffr 11663  ufilen 11664  fmfnfmlem3 11702  fcluscf 11724  filnetlem3 11765  filnetlem4 11766  sstotbnd 11992  bfp 12065

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 145  df-an 223

Copyright terms: Public domain