HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem 3imtr3g 331
Description: More general version of 3imtr3i 327. Useful for converting definitions in a formula. (The proof was shortened by Wolf Lammen, 7-Nov-2012.)
Hypotheses
Ref Expression
3imtr3g.1 |- (ph -> (ps -> ch))
3imtr3g.2 |- (ps <-> th)
3imtr3g.3 |- (ch <-> ta)
Assertion
Ref Expression
3imtr3g |- (ph -> (th -> ta))

Proof of Theorem 3imtr3g
StepHypRef Expression
1 3imtr3g.1 . 2 |- (ph -> (ps -> ch))
2 3imtr3g.2 . . 3 |- (ps <-> th)
32a1i 8 . 2 |- (ph -> (ps <-> th))
4 3imtr3g.3 . . 3 |- (ch <-> ta)
54a1i 8 . 2 |- (ph -> (ch <-> ta))
61, 3, 53imtr3d 329 1 |- (ph -> (th -> ta))
Colors of variables: wff set class
Syntax hints:   -> wi 3   <-> wb 219
This theorem is referenced by:  3imtr4g 332  dvelimfALT 1794  dvelimfALT2 1858  dvelimf 1897  dvelimALT 2008  hblemd 2241  sspwb 3667  wetrep 3805  suceloni 4037  tfinds2 4083  imadif 4593  oprabid 5002  fiint 5872  aceq5lem5 6193  axpowndlem3 6469  lt2msqi 7397  uzind 7760  infxpidmlem12OLD 9226  subtop 9767  dscmet 10062  atabs2i 12805  dfcon2 16266  locfincomp 16338  filfinnfr 16385  prter2 17109  pm11.71 17178  dvelimfALT2OLD 17190
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 220
Copyright terms: Public domain