ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3imtr4d Structured version   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  6650  ltsosr  6652  aptisr  6665  mulextsr1  6667  axpre-mulext  6732  axltwlin  6844  axlttrn  6845  axltadd  6846  axmulgt0  6848  letr  6858  remulext1  7343  mulext1  7356  recexap  7376  prodge0  7561  lt2msq  7593  nnge1  7678  zltp1le  8034  uzss  8229  eluzp1m1  8232  xrletr  8454  ixxssixx  8501  zesq  8980
  Copyright terms: Public domain W3C validator