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

Step	Hyp	Ref	Expression
1		3imtr3d.2	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
2		3imtr3d.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3		3imtr3d.3	. . 3 ⊢ (𝜑 → (𝜒 ↔ 𝜏))
4	2, 3	sylibd 242	. 2 ⊢ (𝜑 → (𝜓 → 𝜏))
5	1, 4	sylbird 263	1 ⊢ (𝜑 → (𝜃 → 𝜏))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  tz6.12i  6909  f1imass  7266  focdmex  7966  tposfn2  8258  naddel1  8690  eroveu  8826  sdomel  9136  ackbij1lem16  10305  ltapr  11123  rpnnen1lem5  13102  qbtwnre  13322  om2uzlt2i  14087  m1dvdsndvds  16969  pcpremul  17014  pcaddlem  17059  pockthlem  17076  prmreclem6  17092  catidd  17847  issgrpd  18912  ghmf1  19453  gexdvds  19791  sylow1lem1  19805  lt6abl  20102  ablfacrplem  20274  isdomn4  20960  drnginvrn0  21005  issrngd  21105  islssd  21203  znrrg  21864  isphld  21953  cnllycmp  25270  nmhmcn  25434  minveclem7  25749  ioorcl2  25886  itg2seq  26056  dvlip2  26308  mdegmullem  26389  plyco0  26503  sincosq1sgn  26820  sincosq2sgn  26821  logcj  26927  argimgt0  26933  lgseisenlem2  27696  leadds1im  28366  leadds1  28368  ltonold  28640  onnolt  28645  addonbday  28658  om2noseqlt2  28679  bdaypw2n0bndlem  28842  remulscllem2  28880  eengtrkg  29557  eengtrkge  29558  ubthlem2  31466  minvecolem7  31478  nmcexi  32621  lnconi  32628  pjnormssi  32763  opsbc2ie  33065  qusvscpbl  33905  tan2h  38515  lindsadd  38516  itg2gt0cn  38573  divrngcl  38871  lshpcmp  40025  cdlemk35s  41974  cdlemk39s  41976  cdlemk42  41978  dihlspsnat  42370  clcnvlem  44608  hashnnltb  45991  tz6.12i-afv2  48282  sqrtnegnre  48346