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

Theorem 3imtr3d 202
Description: More general version of 3imtr3i 200. Useful for converting conditional definitions in a formula. (Contributed by NM, 8-Apr-1996.)
Hypotheses
Ref Expression
3imtr3d.1 (𝜑 → (𝜓𝜒))
3imtr3d.2 (𝜑 → (𝜓𝜃))
3imtr3d.3 (𝜑 → (𝜒𝜏))
Assertion
Ref Expression
3imtr3d (𝜑 → (𝜃𝜏))

Proof of Theorem 3imtr3d
StepHypRef Expression
1 3imtr3d.2 . 2 (𝜑 → (𝜓𝜃))
2 3imtr3d.1 . . 3 (𝜑 → (𝜓𝜒))
3 3imtr3d.3 . . 3 (𝜑 → (𝜒𝜏))
42, 3sylibd 149 . 2 (𝜑 → (𝜓𝜏))
51, 4sylbird 170 1 (𝜑 → (𝜃𝜏))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  f1imass  5796  focdmex  6140  tposfn2  6291  eroveu  6652  ismkvnex  7183  indpi  7371  axcaucvglemres  7928  qsqeqor  10662  caucvgrelemcau  11021  m1dvdsndvds  12280  pcpremul  12325  pcaddlem  12371  pockthlem  12388  issgrpd  12875  ghmf1  13212  islssmd  13675  limccnpcntop  14601  sincosq1sgn  14704  sincosq2sgn  14705  lgseisenlem2  14909  subctctexmid  15209  neap0mkv  15276
  Copyright terms: Public domain W3C validator