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

Theorem 3imtr4g 297
Description: More general version of 3imtr4i 293. 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 (𝜑 → (𝜓𝜒))
3imtr4g.2 (𝜃𝜓)
3imtr4g.3 (𝜏𝜒)
Assertion
Ref Expression
3imtr4g (𝜑 → (𝜃𝜏))

Proof of Theorem 3imtr4g
StepHypRef Expression
1 3imtr4g.2 . . 3 (𝜃𝜓)
2 3imtr4g.1 . . 3 (𝜑 → (𝜓𝜒))
31, 2syl5bi 243 . 2 (𝜑 → (𝜃𝜒))
4 3imtr4g.3 . 2 (𝜏𝜒)
53, 4syl6ibr 253 1 (𝜑 → (𝜃𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207
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 208
This theorem is referenced by:  3anim123d  1436  3orim123d  1437  sbi1  2069  sbequivvOLD  2328  sbimdvOLD  2514  sbimdOLD  2516  moim  2624  mo3  2646  2euswapv  2714  2euswap  2729  exists2  2749  nelcon3d  3140  ral2imi  3161  ralimdv2  3181  rexim  3246  reximdv2  3276  reximd2a  3317  moeq3  3707  rmoim  3735  2reuswap  3741  2reuswap2  3742  2rmoswap  3756  ssel  3965  sstr2  3978  ssrexf  4035  ssrmof  4036  sscon  4119  ssdif  4120  unss1  4159  ssrin  4214  difin0ss  4332  r19.2z  4443  uniss  4858  ssuni  4859  intssuni  4896  iinssiun  4929  iunss1  4930  iinss1  4931  ss2iun  4934  iunxdif3  5014  disjss2  5031  disjss1  5034  disjss3  5062  ssbrd  5106  sspwb  5338  poss  5475  pofun  5490  soss  5492  frss  5521  sess1  5522  sess2  5523  wess  5541  relss  5655  ssrel2  5658  ssrelrel  5668  relop  5720  dmss  5770  dmcosseq  5843  funss  6371  fss  6524  fun  6537  brprcneu  6659  f1eqcocnv  7051  isores3  7080  isomin  7082  isopolem  7090  isosolem  7092  isowe2  7095  ovmpos  7288  dfwe2  7484  onint  7498  orduniorsuc  7533  ordom  7577  finds  7596  finds2  7598  f1oweALT  7664  tposfn2  7905  tposfo2  7906  tposf1o2  7909  smores  7980  tz7.48lem  8068  tz7.48-3  8071  oaass  8177  iiner  8359  xpdom2  8601  ssenen  8680  pssnn  8725  hartogs  8997  card2on  9007  ackbij1  9649  cfub  9660  fin23lem27  9739  fin1a2lem11  9821  fin1a2lem13  9823  hsmexlem2  9838  zorn2lem4  9910  ondomon  9974  gchina  10110  intgru  10225  ingru  10226  addclprlem2  10428  psslinpr  10442  ltexprlem3  10449  ltexprlem4  10450  reclem2pr  10459  suplem1pr  10463  sup2  11586  nnind  11645  nnunb  11882  uzind  12063  xmullem2  12648  xrsupsslem  12690  xrinfmsslem  12691  seqof  13417  hashfacen  13802  sswrd  13859  wrdind  14074  wrd2ind  14075  pfxccatin12lem2  14083  cau3lem  14704  caubnd  14708  sumodd  15729  vdwnnlem2  16322  ramub2  16340  fthres2  17192  odupos  17735  cycsubm  18275  lsmdisj2  18728  gsumxp2  19020  pgpfac1lem3  19119  subrgdvds  19469  lspdisj  19817  lspprat  19845  lbsextlem2  19851  coe1fzgsumd  20389  evl1gsumd  20439  ocv2ss  20736  ocvin  20737  tgcl  21496  epttop  21536  cmpsub  21927  tgcmp  21928  hauscmplem  21933  dfconn2  21946  llyss  22006  nllyss  22007  locfincmp  22053  txcnpi  22135  txcnp  22147  snfil  22391  fgcl  22405  filconn  22410  filuni  22412  cfinfil  22420  csdfil  22421  supfil  22422  ufildom1  22453  fin1aufil  22459  fmfnfmlem3  22483  ptcmplem2  22580  cldsubg  22637  iscau3  23799  iscau4  23800  caussi  23818  volfiniun  24066  plycj  24785  abelth  24947  wilthlem2  25563  lgsdir2lem4  25821  gausslemma2dlem0i  25857  gausslemma2dlem1a  25858  pntleml  26104  uhgr0vsize0  26938  cusgrfilem2  27155  uhgrvd00  27233  clwwisshclwws  27710  frcond3  27965  frgrncvvdeqlem2  27996  lpni  28174  ubthlem1  28564  chintcli  29025  h1de2i  29247  spansnm0i  29344  strlem1  29944  mdslmd1i  30023  reuxfrdf  30172  rabss3d  30193  disjss1f  30240  disjpreima  30252  ssrelf  30284  suppss3  30376  nnindf  30451  wrdt2ind  30544  oduprs  30560  crefss  31002  esumpcvgval  31226  subgrtrl  32267  subgrpth  32268  subgrcycl  32269  derangenlem  32305  connpconn  32369  cvmsss2  32408  pocnv  32886  wzel  32998  fprlem2  33025  sltres  33056  nosupno  33090  nocvxmin  33135  naim1  33624  naim2  33625  waj-ax  33649  lukshef-ax2  33650  bj-eximALT  33861  bj-sbievw1  34056  poimirlem26  34788  poimirlem30  34792  poimirlem32  34794  itg2addnclem  34813  ismtybndlem  34955  ablo4pnp  35029  isdrngo3  35108  keridl  35181  ispridl2  35187  ispridlc  35219  trcoss  35592  funALTVss  35802  disjss  35834  eldisjss  35841  prter1  35885  lshpdisj  35993  snatpsubN  36756  pmapglb2N  36777  pmapglb2xN  36778  elpaddn0  36806  mzpindd  39211  pellexlem3  39296  pellexlem5  39298  pellex  39300  2nn0ind  39410  lnr2i  39584  intabssd  39753  iunrelexpuztr  39932  hess  39994  frege52aid  40072  frege52b  40103  neik0pk1imk0  40265  ichan  43465  nrhmzr  43979  elsetrecslem  44636
  Copyright terms: Public domain W3C validator