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

Theorem 3imtr3d 281
Description: More general version of 3imtr3i 279. 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 228 . 2 (𝜑 → (𝜓𝜏))
51, 4sylbird 249 1 (𝜑 → (𝜃𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195
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 196
This theorem is referenced by:  tz6.12i  6109  f1imass  6400  fornex  7006  tposfn2  7239  eroveu  7707  sdomel  7970  ackbij1lem16  8918  ltapr  9724  rpnnen1lem5  11653  rpnnen1lem5OLD  11659  qbtwnre  11866  om2uzlt2i  12570  m1dvdsndvds  15290  pcpremul  15335  pcaddlem  15379  pockthlem  15396  prmreclem6  15412  catidd  16113  ghmf1  17461  gexdvds  17771  sylow1lem1  17785  lt6abl  18068  ablfacrplem  18236  drnginvrn0  18537  issrngd  18633  islssd  18706  znrrg  19681  isphld  19766  cnllycmp  22511  nmhmcn  22676  minveclem7  22959  ioorcl2  23091  itg2seq  23260  dvlip2  23507  mdegmullem  23587  plyco0  23697  pilem3  23956  sincosq1sgn  23999  sincosq2sgn  24000  logcj  24101  argimgt0  24107  lgseisenlem2  24846  eengtrkg  25611  eengtrkge  25612  ubthlem2  26905  minvecolem7  26917  nmcexi  28063  lnconi  28070  pjnormssi  28205  tan2h  32365  itg2gt0cn  32429  divrngcl  32720  lshpcmp  33087  cdlemk35s  35037  cdlemk39s  35039  cdlemk42  35041  dihlspsnat  35434  clcnvlem  36743
  Copyright terms: Public domain W3C validator