MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3imtr4g Structured version   Unicode version

Theorem 3imtr4g 270
Description: More general version of 3imtr4i 266. Useful for converting definitions in a formula. (Contributed by NM, 20-May-1996.) (Proof shortened by Wolf Lammen, 20-Dec-2013.)
Hypotheses
Ref Expression
3imtr4g.1  |-  ( ph  ->  ( ps  ->  ch ) )
3imtr4g.2  |-  ( th  <->  ps )
3imtr4g.3  |-  ( ta  <->  ch )
Assertion
Ref Expression
3imtr4g  |-  ( ph  ->  ( th  ->  ta ) )

Proof of Theorem 3imtr4g
StepHypRef Expression
1 3imtr4g.2 . . 3  |-  ( th  <->  ps )
2 3imtr4g.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2syl5bi 217 . 2  |-  ( ph  ->  ( th  ->  ch ) )
4 3imtr4g.3 . 2  |-  ( ta  <->  ch )
53, 4syl6ibr 227 1  |-  ( ph  ->  ( th  ->  ta ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
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 185
This theorem is referenced by:  3anim123d  1306  3orim123d  1307  mo3  2320  mo3OLD  2321  moim  2341  morimvOLD  2344  2euswap  2379  ral2imi  2852  ralimOLD  2858  ralimdaaOLD  2867  ralimdv2  2871  rexim  2929  reximdv2  2934  moeq3  3280  rmoim  3303  2reuswap  3306  ssel  3498  sstr2  3511  sscon  3638  ssdif  3639  unss1  3673  ssrin  3723  difin0ss  3893  r19.2z  3917  prel12  4203  uniss  4266  ssuni  4267  intss  4303  intssuni  4304  iunss1  4337  iinss1  4338  ss2iun  4341  disjss2  4420  disjss1  4423  disjss3  4446  ssbrd  4488  reusv6OLD  4658  sspwb  4696  poss  4802  pofun  4816  soss  4818  frss  4846  sess1  4847  sess2  4848  wess  4866  relss  5088  ssrel  5089  ssrel2  5091  ssrelrel  5101  xpsspw  5114  relop  5151  cnvss  5173  dmss  5200  dmcosseq  5262  funss  5604  fss  5737  fun  5746  brprcneu  5857  f1eqcocnv  6190  isores3  6217  isomin  6219  isopolem  6227  isosolem  6229  isowe2  6232  ovmpt2s  6408  dfwe2  6595  onint  6608  orduniorsuc  6643  ordom  6687  finds  6704  finds2  6706  f1oweALT  6765  tposfn2  6974  tposfo2  6975  tposf1o2  6978  smores  7020  tz7.48lem  7103  tz7.48-3  7106  oaass  7207  iiner  7380  xpdom2  7609  ssenen  7688  pssnn  7735  hartogs  7965  card2on  7976  ackbij1  8614  cfub  8625  fin23lem27  8704  fin1a2lem11  8786  fin1a2lem13  8788  hsmexlem2  8803  zorn2lem4  8875  ondomon  8934  gchina  9073  intgru  9188  ingru  9189  addclprlem2  9391  psslinpr  9405  ltexprlem3  9412  ltexprlem4  9413  reclem2pr  9422  suplem1pr  9426  sup2  10495  nnind  10550  nnunb  10787  uzind  10948  xmullem2  11453  xrsupsslem  11494  xrinfmsslem  11495  seqof  12128  hashfacen  12465  sswrd  12517  wrdind  12661  wrd2ind  12662  swrdccatin12lem2  12673  cau3lem  13146  caubnd  13150  vdwnnlem2  14369  ramub2  14387  fthres2  15155  odupos  15618  lsmdisj2  16496  pgpfac1lem3  16918  subrgdvds  17226  lspdisj  17554  lspprat  17582  lbsextlem2  17588  coe1fzgsumd  18115  evl1gsumd  18164  ocv2ss  18471  ocvin  18472  tgcl  19237  epttop  19276  cmpsub  19666  tgcmp  19667  hauscmplem  19672  dfcon2  19686  llyss  19746  nllyss  19747  txcnpi  19844  txcnp  19856  snfil  20100  fgcl  20114  filcon  20119  filuni  20121  cfinfil  20129  csdfil  20130  supfil  20131  ufildom1  20162  fin1aufil  20168  fmfnfmlem3  20192  ptcmplem2  20288  cldsubg  20344  iscau3  21452  iscau4  21453  caussi  21471  volfiniun  21692  plycj  22408  abelth  22570  wilthlem2  23071  lgsdir2lem4  23329  pntleml  23524  cusgrafilem2  24156  frisusgranb  24673  frgrancvvdeqlem3  24709  lpni  24857  ubthlem1  25462  chintcli  25925  h1de2i  26147  spansnm0i  26244  strlem1  26845  mdslmd1i  26924  2reuswap2  27063  ssrmo  27069  rabss3d  27086  disjss1f  27108  disjpreima  27118  ssrelf  27139  nnindf  27278  esumpcvgval  27724  derangenlem  28255  conpcon  28320  cvmsss2  28359  pocnv  28770  wzel  28957  sltres  29001  nocvxmin  29028  naim1  29427  naim2  29428  waj-ax  29456  lukshef-ax2  29457  itg2addnclem  29643  locfincmp  29776  ismtybndlem  29905  ablo4pnp  29945  isdrngo3  29965  keridl  30032  ispridl2  30038  ispridlc  30070  prter1  30224  mzpindd  30282  pellexlem3  30371  pellexlem5  30373  pellex  30375  2nn0ind  30485  lnr2i  30669  ssrexf  30966  2rmoswap  31656  lshpdisj  33784  snatpsubN  34546  pmapglb2N  34567  pmapglb2xN  34568  elpaddn0  34596
  Copyright terms: Public domain W3C validator