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

Theorem 3imtr4d 192
Description: More general version of 3imtr4i 190. 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 158 . 2 (φ → (ψτ))
51, 4sylbid 139 1 (φ → (θτ))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  onsucelsucr  4199  unielrel  4788  ovmpt2s  5566  caofrss  5677  caoftrn  5678  f1o2ndf1  5791  nnaord  6018  nnmord  6026  oviec  6148  ltsopi  6304  lttrsr  6690  ltsosr  6692  aptisr  6705  mulextsr1  6707  axpre-mulext  6772  axltwlin  6884  axlttrn  6885  axltadd  6886  axmulgt0  6888  letr  6898  remulext1  7383  mulext1  7396  recexap  7416  prodge0  7601  lt2msq  7633  nnge1  7718  zltp1le  8074  uzss  8269  eluzp1m1  8272  xrletr  8494  ixxssixx  8541  zesq  9020
  Copyright terms: Public domain W3C validator