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

Theorem 3imtr4g 261
Description: More general version of 3imtr4i 257. 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 208 . 2  |-  ( ph  ->  ( th  ->  ch ) )
4 3imtr4g.3 . 2  |-  ( ta  <->  ch )
53, 4syl6ibr 218 1  |-  ( ph  ->  ( th  ->  ta ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  3anim123d  1259  3orim123d  1260  moim  2189  morimv  2191  2euswap  2219  ralim  2614  ralimdaa  2620  ralimdv2  2623  rexim  2647  reximdv2  2652  moeq3  2942  rmoim  2964  2reuswap  2967  ssel  3174  sstr2  3186  sscon  3310  ssdif  3311  unss1  3344  ssrin  3394  difin0ss  3520  r19.2z  3543  prel12  3789  uniss  3848  ssuni  3849  intss  3883  intssuni  3884  iunss1  3916  iinss1  3917  ss2iun  3920  disjss2  3996  disjss1  3999  disjss3  4022  ssbrd  4064  sspwb  4223  poss  4316  pofun  4330  soss  4332  frss  4360  sess1  4361  sess2  4362  wess  4380  trsuc2OLD  4477  reusv6OLD  4545  dfwe2  4573  onint  4586  orduniorsuc  4621  ordom  4665  finds  4682  finds2  4684  relss  4775  ssrel  4776  ssrelrel  4787  xpsspw  4797  relop  4834  cnvss  4854  dmss  4878  dmcosseq  4946  funss  5273  fss  5397  fun  5405  brprcneu  5518  f1eqcocnv  5805  isores3  5832  isomin  5834  isopolem  5842  isosolem  5844  isowe2  5847  f1oweALT  5851  tposfn2  6256  tposfo2  6257  tposf1o2  6260  smores  6369  tz7.48lem  6453  tz7.48-3  6456  oaass  6559  iiner  6731  xpdom2  6957  ssenen  7035  pssnn  7081  hartogs  7259  card2on  7268  ackbij1  7864  cfub  7875  fin23lem27  7954  fin1a2lem11  8036  fin1a2lem13  8038  hsmexlem2  8053  ondomon  8185  gchina  8321  intgru  8436  ingru  8437  addclprlem2  8641  psslinpr  8655  ltexprlem3  8662  ltexprlem4  8663  reclem2pr  8672  suplem1pr  8676  sup2  9710  nnind  9764  nnunb  9961  uzind  10103  xmullem2  10585  xrsupsslem  10625  xrinfmsslem  10626  seqof  11103  hashfacen  11392  sswrd  11423  wrdind  11477  cau3lem  11838  caubnd  11842  vdwnnlem2  13043  ramub2  13061  fthres2  13806  odupos  14239  lsmdisj2  14991  pgpfac1lem3  15312  subrgdvds  15559  lspdisj  15878  lspprat  15906  lbsextlem2  15912  ocv2ss  16573  ocvin  16574  tgcl  16707  epttop  16746  cmpsub  17127  tgcmp  17128  hauscmplem  17133  dfcon2  17145  llyss  17205  nllyss  17206  txcnpi  17302  txcnp  17314  snfil  17559  fgcl  17573  filcon  17578  filuni  17580  cfinfil  17588  csdfil  17589  supfil  17590  ufildom1  17621  fin1aufil  17627  fmfnfmlem3  17651  ptcmplem2  17747  cldsubg  17793  iscau3  18704  iscau4  18705  caussi  18723  volfiniun  18904  plycj  19658  abelth  19817  wilthlem2  20307  lgsdir2lem4  20565  pntleml  20760  lpni  20846  ubthlem1  21449  chintcli  21910  h1de2i  22132  spansnm0i  22229  strlem1  22830  mdslmd1i  22909  2reuswap2  23137  ssrmo  23148  disjss1f  23351  disjpreima  23361  sigaclfu2  23482  derangenlem  23702  conpcon  23766  cvmsss2  23805  sltres  24318  nocvxmin  24345  naim1  24823  naim2  24824  waj-ax  24853  lukshef-ax2  24854  diaimd  25010  inttop2  25515  qusp  25542  dualded  25783  dualcat2  25784  locfincmp  26304  ismtybndlem  26530  ablo4pnp  26570  isdrngo3  26590  keridl  26657  ispridl2  26663  ispridlc  26695  prter1  26747  mzpindd  26824  pellexlem3  26916  pellexlem5  26918  pellex  26920  2nn0ind  27030  lnr2i  27320  pm10.56  27565  ssrexf  27684  stoweidlem61  27810  2rmoswap  27962  ax12-3  29104  a12stdy1-x12  29111  a12stdy1  29126  a12studyALT  29133  lshpdisj  29177  snatpsubN  29939  pmapglb2N  29960  pmapglb2xN  29961  elpaddn0  29989
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator