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

Theorem 3imtr3g 552
Description: More general version of 3imtr3 218. Useful for converting definitions in a formula.
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 . . . 4 |- (ph -> (ps -> ch))
21imp 350 . . 3 |- ((ph /\ ps) -> ch)
3 3imtr3g.2 . . . 4 |- (ps <-> th)
43anbi2i 480 . . 3 |- ((ph /\ ps) <-> (ph /\ th))
5 3imtr3g.3 . . 3 |- (ch <-> ta)
62, 4, 53imtr3 218 . 2 |- ((ph /\ th) -> ta)
76ex 373 1 |- (ph -> (th -> ta))
Colors of variables: wff set class
Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223
This theorem is referenced by:  3imtr4g 553  dvelimfALT 1153  dvelimf 1250  dvelimALT 1353  sspwb 2755  wetrep 2942  suceloni 3062  tfinds2 3165  imadif 3574  fiint 4559  fiintOLD 4560  aceq5lem5 4739  axpowndlem3 4951  lt2msq 5881  uzind 6205  infxpidmlem12 7563  subtop 7646  dscmet 7918  atabs2 10329
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 147  df-an 225
Copyright terms: Public domain