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 239 . 2 (𝜑 → (𝜓𝜏))
51, 4sylbird 260 1 (𝜑 → (𝜃𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206
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 207
This theorem is referenced by:  tz6.12i  6934  f1imass  7284  focdmex  7980  tposfn2  8273  naddel1  8725  eroveu  8852  sdomel  9164  ackbij1lem16  10274  ltapr  11085  rpnnen1lem5  13023  qbtwnre  13241  om2uzlt2i  13992  m1dvdsndvds  16836  pcpremul  16881  pcaddlem  16926  pockthlem  16943  prmreclem6  16959  catidd  17723  issgrpd  18743  ghmf1  19264  gexdvds  19602  sylow1lem1  19616  lt6abl  19913  ablfacrplem  20085  isdomn4  20716  drnginvrn0  20754  issrngd  20856  islssd  20933  znrrg  21584  isphld  21672  cnllycmp  24988  nmhmcn  25153  minveclem7  25469  ioorcl2  25607  itg2seq  25777  dvlip2  26034  mdegmullem  26117  plyco0  26231  sincosq1sgn  26540  sincosq2sgn  26541  logcj  26648  argimgt0  26654  lgseisenlem2  27420  sleadd1im  28020  sleadd1  28022  sltonold  28283  om2noseqlt2  28306  remulscllem2  28433  eengtrkg  29001  eengtrkge  29002  ubthlem2  30890  minvecolem7  30902  nmcexi  32045  lnconi  32052  pjnormssi  32187  opsbc2ie  32495  qusvscpbl  33379  tan2h  37619  lindsadd  37620  itg2gt0cn  37682  divrngcl  37964  lshpcmp  38989  cdlemk35s  40939  cdlemk39s  40941  cdlemk42  40943  dihlspsnat  41335  clcnvlem  43636  tz6.12i-afv2  47255  sqrtnegnre  47319
  Copyright terms: Public domain W3C validator