HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem 3imtr4d 542
Description: More general version of 3imtr4 219. Useful for converting conditional definitions in a formula.
Hypotheses
Ref Expression
3imtr4d.1 |- (ph -> (ps -> ch))
3imtr4d.2 |- (ph -> (th <-> ps))
3imtr4d.3 |- (ph -> (ta <-> ch))
Assertion
Ref Expression
3imtr4d |- (ph -> (th -> ta))
Proof of Theorem 3imtr4d
StepHypRef Expression
1 3imtr4d.2 . 2 |- (ph -> (th <-> ps))
2 3imtr4d.1 . . 3 |- (ph -> (ps -> ch))
3 3imtr4d.3 . . 3 |- (ph -> (ta <-> ch))
42, 3sylibrd 204 . 2 |- (ph -> (ps -> ta))
51, 4sylbid 203 1 |- (ph -> (th -> ta))
Colors of variables: wff set class
Syntax hints:   -> wi 3   <-> wb 146
This theorem is referenced by:  ax11indalem 1366  ax11inda2ALT 1367  unielrel 3506  fconst5 3839  oaord 4171  omord2 4188  omcan 4190  oeord 4205  oecan 4206  omsmo 4247  oprec 4308  pm54.43 4552  ltsopi 4996  axlttrn 5484  axltadd 5485  axmulgt0 5486  axsup 5487  recext 5665  nnge1t 5899  uzss 6371  eluzp1m1t 6373  expge0t 6530  expge1t 6532  expcant 6540  expordt 6541  expwordit 6542  expword2it 6544  abssubne0t 6828  ser1absdiflem 6874  climsqueeze 7084  climsqueeze2 7085  rescncf 7215  cncffvrn 7216  znnen 7453  tgsst 7586  neips 7677  cnsscnp 7722  ssbl 7807  opnin 7821  metcnss 7850  metcnss2 7851  caussi 7905  lmcau 7946  sqcn 8283  nmcnilem 8285  spwval 8600  spwnex 8602  ocsh 9095  leopaddt 10003  leopmulit 10004  leopmul2it 10006  leoptrt 10008  spansncv2t 10158  mdsl0 10174  ssdmd1 10177  cvdmdt 10201  cdj3 10302  lediv2itALT 10305  truni1 10422  hmphsyma 10451
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
Copyright terms: Public domain