Theorem 3imtr4d 294

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  rmosn  4664  unielrel  6232  predtrss  6280  fvrnressn  7108  fconst5  7154  soisores  7275  caofrss  7663  caoftrn  7665  f1o2ndf1  8065  oaord  8475  omord2  8495  omcan  8497  oeord  8517  oecan  8518  nnaord  8548  nnmord  8561  omsmo  8587  pmss12g  8810  cantnf  9605  pm54.43  9916  ttukeylem2  10423  axlttrn  11209  axltadd  11210  axmulgt0  11211  axsup  11212  ltadd2  11241  ltord1  11667  recex  11773  ltmul1  11996  lt2msq  12032  nnge1  12196  zltp1le  12568  uzss  12802  eluzp1m1  12805  prodge0rd  13042  ixxssixx  13303  zesq  14179  pfxccatin12lem3  14685  swrdccat3blem  14692  relexpsucnnr  14978  climrlim2  15500  rlimres  15511  climshftlem  15527  lo1add  15580  lo1mul  15581  rlimsqzlem  15602  lo1le  15605  isercolllem2  15619  isercoll  15621  climsup  15623  cvgcmp  15770  climcndslem1  15805  dvds1lem  16227  sumodd  16348  rprpwr  16519  algcvg  16536  eucalgcvga  16546  rpexp12i  16685  crth  16739  pc2dvds  16841  pcmpt  16854  prmpwdvds  16866  1arith  16889  vdwlem2  16944  vdwlem6  16948  vdwlem8  16950  ercpbl  17504  initoid  17959  termoid  17960  ipopos  18493  insubm  18777  subginv  19100  symggrp  19366  f1otrspeq  19413  lsmless1x  19610  lsmless2x  19611  dprdss  19997  rngpropd  20146  dvdsunit  20350  irredrmul  20398  isdrngd  20733  isdrngdOLD  20735  lspextmo  21043  rngqiprngimf1lem  21284  domnchr  21522  zntoslem  21546  evlseu  22071  mat2pmatf1  22704  tgss  22943  neips  23088  opnnei  23095  lpss3  23119  ssrest  23151  t1t0  23323  kgen2ss  23530  isfild  23833  fgss  23848  fgss2  23849  cnpflf2  23975  fclsss1  23997  fclsss2  23998  tgpt0  24094  tsmsxp  24130  prdsxmslem2  24504  ngptgp  24611  nghmcn  24720  qdensere  24744  evth  24936  nmhmcn  25097  tcphcph  25214  caussi  25274  equivcfil  25276  rrxmvallem  25381  ivthlem2  25429  ovollb2lem  25465  ovolunlem1  25474  volun  25522  ioombl1lem4  25538  volsup2  25582  volcn  25583  ismbf3d  25631  itg2mulclem  25723  cpnord  25912  lhop1  25991  aaliou3lem2  26320  ulmclm  26365  ulmss  26375  abelth  26419  cosord  26508  efif1olem4  26522  argimgt0  26589  logdivlt  26598  cxploglim  26955  dvdssqf  27115  mumullem1  27156  mumullem2  27157  bposlem6  27266  lgsdchr  27332  gausslemma2dlem1a  27342  m1lgs  27365  chtppilim  27452  lestr  27740  lestric  27746  madebdayim  27894  madebdaylemold  27904  ltslpss  27914  om2noseqf1o  28307  zsoring  28415  bdaypw2n0bndlem  28469  bdayfin  28493  ax5seg  29021  axpasch  29024  axlowdimlem16  29040  axeuclid  29046  axcontlem4  29050  usgr1v0e  29409  nb3gr2nb  29467  cplgr1v  29513  finsumvtxdg2size  29634  usgr2pthlem  29846  clwwlknwwlksn  30123  erclwwlknsym  30155  erclwwlkntr  30156  frgr3vlem1  30358  3vfriswmgrlem  30362  numclwwlk5  30473  minvecolem5  30967  ocsh  31369  shless  31445  leopadd  32218  leopmuli  32219  leopmul2i  32221  leoptr  32223  spansncv2  32379  mdsl0  32396  ssdmd1  32399  cvdmd  32423  cdj3i  32527  uzssico  32872  expgt0b  32905  eqgvscpbl  33425  qusvscpbl  33426  cmpcref  34010  acycgrsubgr  35356  cvmliftmolem1  35479  satffunlem2lem2  35604  mrsubff1  35712  msubff1  35754  lediv2aALT  35875  cgr3tr4  36250  colinearxfr  36273  lineext  36274  brsegle  36306  seglecgr12im  36308  segletr  36312  colinbtwnle  36316  outsideoftr  36327  lineelsb2  36346  ivthALT  36533  tailfb  36575  poimirlem29  37984  itg2addnclem  38006  itg2addnclem3  38008  itg2addnc  38009  incsequz  38083  mettrifi  38092  ismtycnv  38137  bfplem1  38157  ghomco  38226  rngoisocnv  38316  keridl  38367  dmncan1  38411  ax12indalem  39405  ax12inda2ALT  39406  omllaw4  39706  cmtcomlemN  39708  cvlexch2  39789  cvlatexch2  39797  cvrexch  39880  atexchltN  39901  3atlem5  39947  lplnribN  40011  linepsubN  40212  paddss1  40277  paddss2  40278  pmapjoin  40312  pmapjat1  40313  cdleme36a  40920  dib2dim  41703  dih2dimbALTN  41705  djhcvat42  41875  dihjatcclem4  41881  dihjat1lem  41888  lcfrlem6  42007  hlhillcs  42418  oexpreposd  42768  mulgt0b1d  42931  mullt0b1d  42942  pell1234qrmulcl  43301  pell14qrss1234  43302  pell14qrmulcl  43309  pell14qrreccl  43310  pell1qrss14  43314  monotoddzzfi  43388  oddcomabszz  43390  omabs2  43778  omcl3g  43780  tfsconcat0b  43792  naddwordnexlem4  43847  climinf  46054  2ffzoeq  47788  iccpartgt  47899  pgnbgreunbgrlem1  48601  pgnbgreunbgrlem4  48607  upwlkwlk  48627  uspgrsprf1  48635  rrx2xpref1o  49206  itschlc0yqe  49248  resipos  49462