Theorem 3imtr4d 283

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

Hypotheses

Ref	Expression
3imtr4d.1	|- ( ph -> ( ps -> ch ) )
3imtr4d.2	|- ( ph -> ( th <-> ps ) )
3imtr4d.3	|- ( ph -> ( ta <-> ch ) )

Assertion

Ref	Expression
3imtr4d	|- ( ph -> ( th -> ta ) )

Proof of Theorem 3imtr4d

Step	Hyp	Ref	Expression
1		3imtr4d.2	. 2 |- ( ph -> ( th <-> ps ) )
2		3imtr4d.1	. . 3 |- ( ph -> ( ps -> ch ) )
3		3imtr4d.3	. . 3 |- ( ph -> ( ta <-> ch ) )
4	2, 3	sylibrd 249	. 2 |- ( ph -> ( ps -> ta ) )
5	1, 4	sylbid 230	1 |- ( ph -> ( th -> ta ) )

Syntax hints:   -> wi 4   <-> wb 196

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 197

This theorem is referenced by:  unielrel  5660  predpo  5698  fvrnressn  6428  fconst5  6471  soisores  6577  caofrss  6930  caoftrn  6932  f1o2ndf1  7285  oaord  7627  omord2  7647  omcan  7649  oeord  7668  oecan  7669  nnaord  7699  nnmord  7712  omsmo  7734  pmss12g  7884  cantnf  8590  pm54.43  8826  ttukeylem2  9332  axlttrn  10110  axltadd  10111  axmulgt0  10112  axsup  10113  ltadd2  10141  ltord1  10554  recex  10659  prodge0  10870  ltmul1  10873  lt2msq  10908  nnge1  11046  zltp1le  11427  uzss  11708  eluzp1m1  11711  ixxssixx  12189  zesq  12987  swrdccatin12lem3  13490  swrdccat3blem  13495  relexpsucnnr  13765  climrlim2  14278  rlimres  14289  climshftlem  14305  lo1add  14357  lo1mul  14358  rlimsqzlem  14379  lo1le  14382  isercolllem2  14396  isercoll  14398  climsup  14400  cvgcmp  14548  climcndslem1  14581  dvds1lem  14993  sumodd  15111  algcvg  15289  eucalgcvga  15299  rpexp12i  15434  crth  15483  pc2dvds  15583  pcmpt  15596  prmpwdvds  15608  1arith  15631  vdwlem2  15686  vdwlem6  15690  vdwlem8  15692  ercpbl  16209  initoid  16655  termoid  16656  ipopos  17160  subginv  17601  symggrp  17820  f1otrspeq  17867  lsmless1x  18059  lsmless2x  18060  dprdss  18428  dvdsunit  18663  irredrmul  18707  isdrngd  18772  lspextmo  19056  evlseu  19516  domnchr  19880  zntoslem  19905  mat2pmatf1  20534  tgss  20772  neips  20917  opnnei  20924  lpss3  20948  ssrest  20980  t1t0  21152  kgen2ss  21358  isfild  21662  fgss  21677  fgss2  21678  cnpflf2  21804  fclsss1  21826  fclsss2  21827  tgpt0  21922  tsmsxp  21958  prdsxmslem2  22334  ngptgp  22440  nghmcn  22549  qdensere  22573  evth  22758  nmhmcn  22920  tchcph  23036  caussi  23095  equivcfil  23097  rrxmvallem  23187  ivthlem2  23221  ovollb2lem  23256  ovolunlem1  23265  volun  23313  ioombl1lem4  23329  volsup2  23373  volcn  23374  ismbf3d  23421  itg2mulclem  23513  cpnord  23698  lhop1  23777  aaliou3lem2  24098  ulmclm  24141  ulmss  24151  abelth  24195  cosord  24278  efif1olem4  24291  argimgt0  24358  logdivlt  24367  cxploglim  24704  dvdssqf  24864  mumullem1  24905  mumullem2  24906  bposlem6  25014  lgsdchr  25080  gausslemma2dlem1a  25090  m1lgs  25113  chtppilim  25164  ax5seg  25818  axpasch  25821  axlowdimlem16  25837  axeuclid  25843  axcontlem4  25847  usgr1v0e  26218  nb3gr2nb  26286  cplgr1v  26326  finsumvtxdg2size  26446  usgr2pthlem  26659  erclwwlksnsym  26947  erclwwlksntr  26948  clwlksfclwwlk  26962  frgr3vlem1  27137  3vfriswmgrlem  27141  numclwwlk5  27246  minvecolem5  27737  ocsh  28142  shless  28218  leopadd  28991  leopmuli  28992  leopmul2i  28994  leoptr  28996  spansncv2  29152  mdsl0  29169  ssdmd1  29172  cvdmd  29196  cdj3i  29300  uzssico  29546  cmpcref  29917  cvmliftmolem1  31263  mrsubff1  31411  msubff1  31453  lediv2aALT  31571  sletr  31883  cgr3tr4  32159  colinearxfr  32182  lineext  32183  brsegle  32215  seglecgr12im  32217  segletr  32221  colinbtwnle  32225  outsideoftr  32236  lineelsb2  32255  ivthALT  32330  tailfb  32372  poimirlem29  33438  itg2addnclem  33461  itg2addnclem3  33463  itg2addnc  33464  incsequz  33544  mettrifi  33553  ismtycnv  33601  bfplem1  33621  ghomco  33690  rngoisocnv  33780  keridl  33831  dmncan1  33875  ax12indalem  34230  ax12inda2ALT  34231  omllaw4  34533  cmtcomlemN  34535  cvlexch2  34616  cvlatexch2  34624  cvrexch  34706  atexchltN  34727  3atlem5  34773  lplnribN  34837  linepsubN  35038  paddss1  35103  paddss2  35104  pmapjoin  35138  pmapjat1  35139  cdleme36a  35748  dib2dim  36532  dih2dimbALTN  36534  djhcvat42  36704  dihjatcclem4  36710  dihjat1lem  36717  lcfrlem6  36836  hlhillcs  37250  pell1234qrmulcl  37419  pell14qrss1234  37420  pell14qrmulcl  37427  pell14qrreccl  37428  pell1qrss14  37432  monotoddzzfi  37507  oddcomabszz  37509  climinf  39838  2ffzoeq  41338  iccpartgt  41363  upwlkwlk  41720  uspgrsprf1  41755