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

Theorem 3imtr3d 296
Description: More general version of 3imtr3i 294. 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 242 . 2 (𝜑 → (𝜓𝜏))
51, 4sylbird 263 1 (𝜑 → (𝜃𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209
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 210
This theorem is referenced by:  tz6.12i  6700  f1imass  7033  fornex  7682  tposfn2  7943  eroveu  8423  sdomel  8714  ackbij1lem16  9735  ltapr  10545  rpnnen1lem5  12463  qbtwnre  12675  om2uzlt2i  13410  m1dvdsndvds  16235  pcpremul  16280  pcaddlem  16324  pockthlem  16341  prmreclem6  16357  catidd  17054  ghmf1  18505  gexdvds  18827  sylow1lem1  18841  lt6abl  19134  ablfacrplem  19306  drnginvrn0  19639  issrngd  19751  islssd  19826  znrrg  20384  isphld  20470  cnllycmp  23708  nmhmcn  23872  minveclem7  24187  ioorcl2  24324  itg2seq  24495  dvlip2  24747  mdegmullem  24831  plyco0  24941  sincosq1sgn  25243  sincosq2sgn  25244  logcj  25349  argimgt0  25355  lgseisenlem2  26112  eengtrkg  26932  eengtrkge  26933  ubthlem2  28806  minvecolem7  28818  nmcexi  29961  lnconi  29968  pjnormssi  30103  opsbc2ie  30398  qusvscpbl  31123  naddel1  33480  tan2h  35392  lindsadd  35393  itg2gt0cn  35455  divrngcl  35738  lshpcmp  36625  cdlemk35s  38574  cdlemk39s  38576  cdlemk42  38578  dihlspsnat  38970  isdomn4  39763  clcnvlem  40776  tz6.12i-afv2  44268  sqrtnegnre  44333
  Copyright terms: Public domain W3C validator