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  4183  unielrel  4772  ovmpt2s  5547  caofrss  5658  caoftrn  5659  f1o2ndf1  5772  nnaord  5993  nnmord  6001  oviec  6123  ltsopi  6180  lttrsr  6509  ltsosr  6511  axltwlin  6688  axlttrn  6689  axltadd  6690  axmulgt0  6691  letr  6699
  Copyright terms: Public domain W3C validator