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  4492  unielrel  5138  ovmpos  5976  caofrss  6085  caoftrn  6086  f1o2ndf1  6207  nnaord  6488  nnmord  6496  oviec  6619  pmss12g  6653  fiss  6954  pm54.43  7167  ltsopi  7282  lttrsr  7724  ltsosr  7726  aptisr  7741  mulextsr1  7743  axpre-mulext  7850  axltwlin  7987  axlttrn  7988  axltadd  7989  axmulgt0  7991  letr  8002  eqord1  8402  remulext1  8518  mulext1  8531  recexap  8571  prodge0  8770  lt2msq  8802  nnge1  8901  zltp1le  9266  uzss  9507  eluzp1m1  9510  xrletr  9765  ixxssixx  9859  zesq  10594  expcanlem  10649  expcan  10650  nn0opthd  10656  maxleast  11177  climshftlemg  11265  dvds1lem  11764  bezoutlemzz  11957  algcvg  12002  eucalgcvga  12012  rpexp12i  12109  crth  12178  pc2dvds  12283  pcmpt  12295  prmpwdvds  12307  1arith  12319  insubm  12703  tgss  12857  neipsm  12948  ssrest  12976  cos11  13568  lgsdir2lem4  13726
  Copyright terms: Public domain W3C validator