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

Theorem 3imtr4d 196
 Description: More general version of 3imtr4i 194. 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 162 . 2 (𝜑 → (𝜓𝜏))
51, 4sylbid 143 1 (𝜑 → (𝜃𝜏))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 102 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  onsucelsucr  4262  unielrel  4873  ovmpt2s  5652  caofrss  5763  caoftrn  5764  f1o2ndf1  5877  nnaord  6113  nnmord  6121  oviec  6243  ltsopi  6476  lttrsr  6905  ltsosr  6907  aptisr  6921  mulextsr1  6923  axpre-mulext  7020  axltwlin  7146  axlttrn  7147  axltadd  7148  axmulgt0  7150  letr  7160  remulext1  7664  mulext1  7677  recexap  7708  prodge0  7895  lt2msq  7927  nnge1  8013  zltp1le  8356  uzss  8589  eluzp1m1  8592  xrletr  8825  ixxssixx  8872  zesq  9535  nn0opthd  9590  climshftlemg  10054  dvds1lem  10119  ialgcvg  10270
 Copyright terms: Public domain W3C validator