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

Theorem 3imtr4d 202
Description: More general version of 3imtr4i 200. 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 168 . 2 (𝜑 → (𝜓𝜏))
51, 4sylbid 149 1 (𝜑 → (𝜃𝜏))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  onsucelsucr  4353  unielrel  4992  ovmpt2s  5806  caofrss  5917  caoftrn  5918  f1o2ndf1  6031  nnaord  6308  nnmord  6316  oviec  6438  pmss12g  6472  pm54.43  6915  ltsopi  6976  lttrsr  7405  ltsosr  7407  aptisr  7421  mulextsr1  7423  axpre-mulext  7520  axltwlin  7651  axlttrn  7652  axltadd  7653  axmulgt0  7655  letr  7665  eqord1  8058  remulext1  8173  mulext1  8186  recexap  8219  prodge0  8412  lt2msq  8444  nnge1  8543  zltp1le  8902  uzss  9138  eluzp1m1  9141  xrletr  9374  ixxssixx  9468  zesq  10187  expcanlem  10239  expcan  10240  nn0opthd  10245  maxleast  10761  climshftlemg  10845  efler  11138  dvds1lem  11234  bezoutlemzz  11418  algcvg  11457  eucalgcvga  11467  rpexp12i  11561  crth  11627  tgss  11915  neipsm  12006  ssrest  12034
  Copyright terms: Public domain W3C validator