MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3imtr3d Structured version   Visualization version   GIF version

Theorem 3imtr3d 293
Description: More general version of 3imtr3i 291. 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 238 . 2 (𝜑 → (𝜓𝜏))
51, 4sylbird 259 1 (𝜑 → (𝜃𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 206
This theorem is referenced by:  tz6.12i  6800  f1imass  7137  fornex  7798  tposfn2  8064  eroveu  8601  sdomel  8911  ackbij1lem16  9991  ltapr  10801  rpnnen1lem5  12721  qbtwnre  12933  om2uzlt2i  13671  m1dvdsndvds  16499  pcpremul  16544  pcaddlem  16589  pockthlem  16606  prmreclem6  16622  catidd  17389  ghmf1  18863  gexdvds  19189  sylow1lem1  19203  lt6abl  19496  ablfacrplem  19668  drnginvrn0  20009  issrngd  20121  islssd  20197  znrrg  20773  isphld  20859  cnllycmp  24119  nmhmcn  24283  minveclem7  24599  ioorcl2  24736  itg2seq  24907  dvlip2  25159  mdegmullem  25243  plyco0  25353  sincosq1sgn  25655  sincosq2sgn  25656  logcj  25761  argimgt0  25767  lgseisenlem2  26524  eengtrkg  27354  eengtrkge  27355  ubthlem2  29233  minvecolem7  29245  nmcexi  30388  lnconi  30395  pjnormssi  30530  opsbc2ie  30824  qusvscpbl  31551  naddel1  33839  tan2h  35769  lindsadd  35770  itg2gt0cn  35832  divrngcl  36115  lshpcmp  37002  cdlemk35s  38951  cdlemk39s  38953  cdlemk42  38955  dihlspsnat  39347  isdomn4  40172  clcnvlem  41231  tz6.12i-afv2  44735  sqrtnegnre  44799
  Copyright terms: Public domain W3C validator