ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3imtr4d GIF version

Theorem 3imtr4d 202
Description: More general version of 3imtr4i 200. Useful for converting conditional definitions in a formula. (Contributed by NM, 26-Oct-1995.)
Hypotheses
Ref Expression
3imtr4d.1 (𝜑 → (𝜓𝜒))
3imtr4d.2 (𝜑 → (𝜃𝜓))
3imtr4d.3 (𝜑 → (𝜏𝜒))
Assertion
Ref Expression
3imtr4d (𝜑 → (𝜃𝜏))

Proof of Theorem 3imtr4d
StepHypRef Expression
1 3imtr4d.2 . 2 (𝜑 → (𝜃𝜓))
2 3imtr4d.1 . . 3 (𝜑 → (𝜓𝜒))
3 3imtr4d.3 . . 3 (𝜑 → (𝜏𝜒))
42, 3sylibrd 168 . 2 (𝜑 → (𝜓𝜏))
51, 4sylbid 149 1 (𝜑 → (𝜃𝜏))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  onsucelsucr  4394  unielrel  5036  ovmpos  5862  caofrss  5974  caoftrn  5975  f1o2ndf1  6093  nnaord  6373  nnmord  6381  oviec  6503  pmss12g  6537  fiss  6833  pm54.43  7014  ltsopi  7096  lttrsr  7538  ltsosr  7540  aptisr  7555  mulextsr1  7557  axpre-mulext  7664  axltwlin  7800  axlttrn  7801  axltadd  7802  axmulgt0  7804  letr  7815  eqord1  8213  remulext1  8329  mulext1  8342  recexap  8382  prodge0  8580  lt2msq  8612  nnge1  8711  zltp1le  9076  uzss  9314  eluzp1m1  9317  xrletr  9559  ixxssixx  9653  zesq  10378  expcanlem  10430  expcan  10431  nn0opthd  10436  maxleast  10953  climshftlemg  11039  efler  11332  dvds1lem  11431  bezoutlemzz  11617  algcvg  11656  eucalgcvga  11666  rpexp12i  11760  crth  11827  tgss  12159  neipsm  12250  ssrest  12278
  Copyright terms: Public domain W3C validator