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  4234  unielrel  4845  ovmpt2s  5624  caofrss  5735  caoftrn  5736  f1o2ndf1  5849  nnaord  6082  nnmord  6090  oviec  6212  ltsopi  6418  lttrsr  6847  ltsosr  6849  aptisr  6863  mulextsr1  6865  axpre-mulext  6962  axltwlin  7087  axlttrn  7088  axltadd  7089  axmulgt0  7091  letr  7101  remulext1  7590  mulext1  7603  recexap  7634  prodge0  7820  lt2msq  7852  nnge1  7937  zltp1le  8298  uzss  8493  eluzp1m1  8496  xrletr  8724  ixxssixx  8771  zesq  9367  climshftlemg  9823  ialgcvg  9887
 Copyright terms: Public domain W3C validator