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 ⊢ (𝜑 → (𝜃 → 𝜏))

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:  rmosn  4682  unielrel  6300  predtrss  6351  fvrnressn  7197  fconst5  7243  soisores  7366  caofrss  7764  caoftrn  7766  f1o2ndf1  8170  oaord  8593  omord2  8613  omcan  8615  oeord  8635  oecan  8636  nnaord  8666  nnmord  8679  omsmo  8705  pmss12g  8935  cantnf  9731  pm54.43  10121  ttukeylem2  10627  axlttrn  11421  axltadd  11422  axmulgt0  11423  axsup  11424  ltadd2  11453  ltord1  11882  recex  11988  ltmul1  12207  lt2msq  12242  nnge1  12406  zltp1le  12786  uzss  13028  eluzp1m1  13031  prodge0rd  13269  ixxssixx  13530  zesq  14411  pfxccatin12lem3  14923  swrdccat3blem  14930  relexpsucnnr  15221  climrlim2  15758  rlimres  15769  climshftlem  15785  lo1add  15838  lo1mul  15839  rlimsqzlem  15860  lo1le  15863  isercolllem2  15877  isercoll  15879  climsup  15881  cvgcmp  16027  climcndslem1  16062  dvds1lem  16481  sumodd  16602  rprpwr  16777  algcvg  16795  eucalgcvga  16805  rpexp12i  16944  crth  16999  pc2dvds  17101  pcmpt  17114  prmpwdvds  17126  1arith  17149  vdwlem2  17204  vdwlem6  17208  vdwlem8  17210  ercpbl  17771  initoid  18226  termoid  18227  ipopos  18760  insubm  19064  subginv  19393  symggrp  19665  f1otrspeq  19712  lsmless1x  19909  lsmless2x  19910  dprdss  20296  rngpropd  20447  dvdsunit  20660  irredrmul  20708  isdrngd  21073  isdrngdOLD  21075  lspextmo  21382  rngqiprngimf1lem  21641  domnchr  21893  zntoslem  21917  evlseu  22447  mat2pmatf1  23102  tgss  23341  neips  23486  opnnei  23493  lpss3  23517  ssrest  23549  t1t0  23721  kgen2ss  23929  isfild  24232  fgss  24247  fgss2  24248  cnpflf2  24374  fclsss1  24396  fclsss2  24397  tgpt0  24493  tsmsxp  24529  prdsxmslem2  24903  ngptgp  25010  nghmcn  25119  qdensere  25143  evth  25335  nmhmcn  25496  tcphcph  25613  caussi  25673  equivcfil  25675  rrxmvallem  25780  ivthlem2  25828  ovollb2lem  25864  ovolunlem1  25873  volun  25921  ioombl1lem4  25937  volsup2  25981  volcn  25982  ismbf3d  26030  itg2mulclem  26122  cpnord  26310  lhop1  26389  aaliou3lem2  26727  ulmclm  26771  ulmss  26781  abelth  26825  cosord  26916  efif1olem4  26930  argimgt0  26997  logdivlt  27006  cxploglim  27362  dvdssqf  27522  mumullem1  27563  mumullem2  27564  bposlem6  27673  lgsdchr  27739  gausslemma2dlem1a  27749  m1lgs  27772  chtppilim  27859  lestr  28176  lestric  28182  madebdayim  28331  madebdaylemold  28341  ltslpss  28351  om2noseqf1o  28744  zsoring  28852  bdaypw2n0bndlem  28906  bdayfin  28930  ax5seg  29573  axpasch  29576  axlowdimlem16  29592  axeuclid  29598  axcontlem4  29602  usgr1v0e  29964  nb3gr2nb  30022  cplgr1v  30068  finsumvtxdg2size  30188  usgr2pthlem  30406  clwwlknwwlksn  30686  erclwwlknsym  30718  erclwwlkntr  30719  frgr3vlem1  30931  3vfriswmgrlem  30935  numclwwlk5  31046  minvecolem5  31540  ocsh  31942  shless  32018  leopadd  32791  leopmuli  32792  leopmul2i  32794  leoptr  32796  spansncv2  32952  mdsl0  32969  ssdmd1  32972  cvdmd  32996  cdj3i  33100  uzssico  33472  expgt0b  33504  eqgvscpbl  34015  qusvscpbl  34016  cmpcref  34593  acycgrsubgr  36121  cvmliftmolem1  36254  satffunlem2lem2  36379  mrsubff1  36487  msubff1  36529  lediv2aALT  36650  cgr3tr4  37032  colinearxfr  37055  lineext  37056  brsegle  37088  seglecgr12im  37090  segletr  37094  colinbtwnle  37098  outsideoftr  37109  lineelsb2  37128  ltnmul  37180  ltnadd  37182  ivthALT  37338  tailfb  37380  poimirlem29  38835  itg2addnclem  38857  itg2addnclem3  38859  itg2addnc  38860  incsequz  38948  mettrifi  38957  ismtycnv  39002  bfplem1  39022  ghomco  39091  rngoisocnv  39181  keridl  39232  dmncan1  39276  ax12indalem  40268  ax12inda2ALT  40269  omllaw4  40569  cmtcomlemN  40571  cvlexch2  40652  cvlatexch2  40660  cvrexch  40743  atexchltN  40764  3atlem5  40810  lplnribN  40874  linepsubN  41075  paddss1  41140  paddss2  41141  pmapjoin  41175  pmapjat1  41176  cdleme36a  41783  dib2dim  42566  dih2dimbALTN  42568  djhcvat42  42738  dihjatcclem4  42744  dihjat1lem  42751  lcfrlem6  42870  hlhillcs  43281  oexpreposd  43645  mulgt0b1d  43802  mullt0b1d  43813  pell1234qrmulcl  44128  pell14qrss1234  44129  pell14qrmulcl  44136  pell14qrreccl  44137  pell1qrss14  44141  monotoddzzfi  44215  oddcomabszz  44217  omabs2  44595  omcl3g  44597  tfsconcat0b  44609  naddwordnexlem4  44664  climinf  46891  2ffzoeq  48671  iccpartgt  48782  pgnbgreunbgrlem1  49484  pgnbgreunbgrlem4  49490  upwlkwlk  49510  uspgrsprf1  49518  idomcanl  49775  itschlc0yqe  50203  resipos  50420