Theorem 3imtr4d 296

Description: More general version of 3imtr4i 294. 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 261	. 2 ⊢ (𝜑 → (𝜓 → 𝜏))
5	1, 4	sylbid 242	1 ⊢ (𝜑 → (𝜃 → 𝜏))

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  rmosn  4647  unielrel  6118  predpo  6159  fvrnressn  6916  fconst5  6961  soisores  7072  caofrss  7434  caoftrn  7436  f1o2ndf1  7810  oaord  8165  omord2  8185  omcan  8187  oeord  8206  oecan  8207  nnaord  8237  nnmord  8250  omsmo  8273  pmss12g  8425  cantnf  9148  pm54.43  9421  ttukeylem2  9924  axlttrn  10705  axltadd  10706  axmulgt0  10707  axsup  10708  ltadd2  10736  ltord1  11158  recex  11264  ltmul1  11482  lt2msq  11517  nnge1  11657  zltp1le  12024  uzss  12257  eluzp1m1  12260  prodge0rd  12488  ixxssixx  12744  zesq  13579  pfxccatin12lem3  14086  swrdccat3blem  14093  relexpsucnnr  14376  climrlim2  14896  rlimres  14907  climshftlem  14923  lo1add  14975  lo1mul  14976  rlimsqzlem  14997  lo1le  15000  isercolllem2  15014  isercoll  15016  climsup  15018  cvgcmp  15163  climcndslem1  15196  dvds1lem  15613  sumodd  15731  algcvg  15912  eucalgcvga  15922  rpexp12i  16058  crth  16107  pc2dvds  16207  pcmpt  16220  prmpwdvds  16232  1arith  16255  vdwlem2  16310  vdwlem6  16314  vdwlem8  16316  ercpbl  16814  initoid  17257  termoid  17258  ipopos  17762  insubm  17975  subginv  18278  symggrp  18520  f1otrspeq  18567  lsmless1x  18761  lsmless2x  18762  dprdss  19143  dvdsunit  19405  irredrmul  19449  isdrngd  19519  lspextmo  19820  evlseu  20288  domnchr  20671  zntoslem  20695  mat2pmatf1  21329  tgss  21568  neips  21713  opnnei  21720  lpss3  21744  ssrest  21776  t1t0  21948  kgen2ss  22155  isfild  22458  fgss  22473  fgss2  22474  cnpflf2  22600  fclsss1  22622  fclsss2  22623  tgpt0  22719  tsmsxp  22755  prdsxmslem2  23131  ngptgp  23237  nghmcn  23346  qdensere  23370  evth  23555  nmhmcn  23716  tcphcph  23832  caussi  23892  equivcfil  23894  rrxmvallem  23999  ivthlem2  24045  ovollb2lem  24081  ovolunlem1  24090  volun  24138  ioombl1lem4  24154  volsup2  24198  volcn  24199  ismbf3d  24247  itg2mulclem  24339  cpnord  24524  lhop1  24603  aaliou3lem2  24924  ulmclm  24967  ulmss  24977  abelth  25021  cosord  25108  efif1olem4  25121  argimgt0  25187  logdivlt  25196  cxploglim  25547  dvdssqf  25707  mumullem1  25748  mumullem2  25749  bposlem6  25857  lgsdchr  25923  gausslemma2dlem1a  25933  m1lgs  25956  chtppilim  26043  ax5seg  26716  axpasch  26719  axlowdimlem16  26735  axeuclid  26741  axcontlem4  26745  usgr1v0e  27100  nb3gr2nb  27158  cplgr1v  27204  finsumvtxdg2size  27324  usgr2pthlem  27536  clwwlknwwlksn  27808  erclwwlknsym  27841  erclwwlkntr  27842  frgr3vlem1  28044  3vfriswmgrlem  28048  numclwwlk5  28159  minvecolem5  28650  ocsh  29052  shless  29128  leopadd  29901  leopmuli  29902  leopmul2i  29904  leoptr  29906  spansncv2  30062  mdsl0  30079  ssdmd1  30082  cvdmd  30106  cdj3i  30210  uzssico  30499  eqgvscpbl  30912  qusvscpbl  30913  cmpcref  31107  acycgrsubgr  32398  cvmliftmolem1  32521  satffunlem2lem2  32646  mrsubff1  32754  msubff1  32796  lediv2aALT  32913  sletr  33230  cgr3tr4  33506  colinearxfr  33529  lineext  33530  brsegle  33562  seglecgr12im  33564  segletr  33568  colinbtwnle  33572  outsideoftr  33583  lineelsb2  33602  ivthALT  33676  tailfb  33718  poimirlem29  34913  itg2addnclem  34935  itg2addnclem3  34937  itg2addnc  34938  incsequz  35015  mettrifi  35024  ismtycnv  35072  bfplem1  35092  ghomco  35161  rngoisocnv  35251  keridl  35302  dmncan1  35346  ax12indalem  36073  ax12inda2ALT  36074  omllaw4  36374  cmtcomlemN  36376  cvlexch2  36457  cvlatexch2  36465  cvrexch  36548  atexchltN  36569  3atlem5  36615  lplnribN  36679  linepsubN  36880  paddss1  36945  paddss2  36946  pmapjoin  36980  pmapjat1  36981  cdleme36a  37588  dib2dim  38371  dih2dimbALTN  38373  djhcvat42  38543  dihjatcclem4  38549  dihjat1lem  38556  lcfrlem6  38675  hlhillcs  39086  oexpreposd  39170  pell1234qrmulcl  39443  pell14qrss1234  39444  pell14qrmulcl  39451  pell14qrreccl  39452  pell1qrss14  39456  monotoddzzfi  39530  oddcomabszz  39532  climinf  41877  2ffzoeq  43519  iccpartgt  43578  upwlkwlk  44005  uspgrsprf1  44013  rrx2xpref1o  44696  itschlc0yqe  44738