Theorem 3imtr4d 297

Description: More general version of 3imtr4i 295. Useful for converting conditional definitions in a formula. (Contributed by NM, 26-Oct-1995.)

Hypotheses

Ref	Expression
3imtr4d.1	⊢ (𝜑 → (𝜓 → 𝜒))
3imtr4d.2	⊢ (𝜑 → (𝜃 ↔ 𝜓))
3imtr4d.3	⊢ (𝜑 → (𝜏 ↔ 𝜒))

Assertion

Ref	Expression
3imtr4d	⊢ (𝜑 → (𝜃 → 𝜏))

Proof of Theorem 3imtr4d

Step	Hyp	Ref	Expression
1		3imtr4d.2	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜓))
2		3imtr4d.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3		3imtr4d.3	. . 3 ⊢ (𝜑 → (𝜏 ↔ 𝜒))
4	2, 3	sylibrd 262	. 2 ⊢ (𝜑 → (𝜓 → 𝜏))
5	1, 4	sylbid 243	1 ⊢ (𝜑 → (𝜃 → 𝜏))

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:  rmosn  4620  unielrel  6116  predpo  6157  fvrnressn  6946  fconst5  6991  soisores  7106  caofrss  7473  caoftrn  7475  f1o2ndf1  7857  oaord  8217  omord2  8237  omcan  8239  oeord  8258  oecan  8259  nnaord  8289  nnmord  8302  omsmo  8325  pmss12g  8492  cantnf  9242  pm54.43  9516  ttukeylem2  10023  axlttrn  10804  axltadd  10805  axmulgt0  10806  axsup  10807  ltadd2  10835  ltord1  11257  recex  11363  ltmul1  11581  lt2msq  11616  nnge1  11757  zltp1le  12126  uzss  12360  eluzp1m1  12363  prodge0rd  12592  ixxssixx  12848  zesq  13692  pfxccatin12lem3  14196  swrdccat3blem  14203  relexpsucnnr  14487  climrlim2  15007  rlimres  15018  climshftlem  15034  lo1add  15087  lo1mul  15088  rlimsqzlem  15111  lo1le  15114  isercolllem2  15128  isercoll  15130  climsup  15132  cvgcmp  15277  climcndslem1  15310  dvds1lem  15726  sumodd  15846  rprpwr  16017  algcvg  16030  eucalgcvga  16040  rpexp12i  16178  crth  16228  pc2dvds  16328  pcmpt  16341  prmpwdvds  16353  1arith  16376  vdwlem2  16431  vdwlem6  16435  vdwlem8  16437  ercpbl  16938  initoid  17386  termoid  17387  ipopos  17899  insubm  18112  subginv  18417  symggrp  18659  f1otrspeq  18706  lsmless1x  18900  lsmless2x  18901  dprdss  19283  dvdsunit  19548  irredrmul  19592  isdrngd  19659  lspextmo  19960  domnchr  20364  zntoslem  20388  evlseu  20910  mat2pmatf1  21493  tgss  21732  neips  21877  opnnei  21884  lpss3  21908  ssrest  21940  t1t0  22112  kgen2ss  22319  isfild  22622  fgss  22637  fgss2  22638  cnpflf2  22764  fclsss1  22786  fclsss2  22787  tgpt0  22883  tsmsxp  22919  prdsxmslem2  23295  ngptgp  23402  nghmcn  23511  qdensere  23535  evth  23724  nmhmcn  23885  tcphcph  24002  caussi  24062  equivcfil  24064  rrxmvallem  24169  ivthlem2  24217  ovollb2lem  24253  ovolunlem1  24262  volun  24310  ioombl1lem4  24326  volsup2  24370  volcn  24371  ismbf3d  24419  itg2mulclem  24512  cpnord  24700  lhop1  24779  aaliou3lem2  25104  ulmclm  25147  ulmss  25157  abelth  25201  cosord  25288  efif1olem4  25302  argimgt0  25368  logdivlt  25377  cxploglim  25728  dvdssqf  25888  mumullem1  25929  mumullem2  25930  bposlem6  26038  lgsdchr  26104  gausslemma2dlem1a  26114  m1lgs  26137  chtppilim  26224  ax5seg  26897  axpasch  26900  axlowdimlem16  26916  axeuclid  26922  axcontlem4  26926  usgr1v0e  27281  nb3gr2nb  27339  cplgr1v  27385  finsumvtxdg2size  27505  usgr2pthlem  27717  clwwlknwwlksn  27988  erclwwlknsym  28020  erclwwlkntr  28021  frgr3vlem1  28223  3vfriswmgrlem  28227  numclwwlk5  28338  minvecolem5  28829  ocsh  29231  shless  29307  leopadd  30080  leopmuli  30081  leopmul2i  30083  leoptr  30085  spansncv2  30241  mdsl0  30258  ssdmd1  30261  cvdmd  30285  cdj3i  30389  uzssico  30693  eqgvscpbl  31135  qusvscpbl  31136  cmpcref  31385  acycgrsubgr  32704  cvmliftmolem1  32827  satffunlem2lem2  32952  mrsubff1  33060  msubff1  33102  lediv2aALT  33219  sletr  33617  madebdayim  33726  madebdaylemold  33734  sltlpss  33743  cgr3tr4  34010  colinearxfr  34033  lineext  34034  brsegle  34066  seglecgr12im  34068  segletr  34072  colinbtwnle  34076  outsideoftr  34087  lineelsb2  34106  ivthALT  34180  tailfb  34222  poimirlem29  35462  itg2addnclem  35484  itg2addnclem3  35486  itg2addnc  35487  incsequz  35562  mettrifi  35571  ismtycnv  35616  bfplem1  35636  ghomco  35705  rngoisocnv  35795  keridl  35846  dmncan1  35890  ax12indalem  36615  ax12inda2ALT  36616  omllaw4  36916  cmtcomlemN  36918  cvlexch2  36999  cvlatexch2  37007  cvrexch  37090  atexchltN  37111  3atlem5  37157  lplnribN  37221  linepsubN  37422  paddss1  37487  paddss2  37488  pmapjoin  37522  pmapjat1  37523  cdleme36a  38130  dib2dim  38913  dih2dimbALTN  38915  djhcvat42  39085  dihjatcclem4  39091  dihjat1lem  39098  lcfrlem6  39217  hlhillcs  39628  oexpreposd  39938  mulgt0b2d  40048  pell1234qrmulcl  40290  pell14qrss1234  40291  pell14qrmulcl  40298  pell14qrreccl  40299  pell1qrss14  40303  monotoddzzfi  40377  oddcomabszz  40379  climinf  42730  2ffzoeq  44402  iccpartgt  44461  upwlkwlk  44883  uspgrsprf1  44891  rrx2xpref1o  45646  itschlc0yqe  45688