ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3bitr4g GIF version

Theorem 3bitr4g 222
Description: More general version of 3bitr4i 211. Useful for converting definitions in a formula. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
3bitr4g.1 (𝜑 → (𝜓𝜒))
3bitr4g.2 (𝜃𝜓)
3bitr4g.3 (𝜏𝜒)
Assertion
Ref Expression
3bitr4g (𝜑 → (𝜃𝜏))

Proof of Theorem 3bitr4g
StepHypRef Expression
1 3bitr4g.2 . . 3 (𝜃𝜓)
2 3bitr4g.1 . . 3 (𝜑 → (𝜓𝜒))
31, 2syl5bb 191 . 2 (𝜑 → (𝜃𝜒))
4 3bitr4g.3 . 2 (𝜏𝜒)
53, 4syl6bbr 197 1 (𝜑 → (𝜃𝜏))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  bibi1d  232  pm5.32rd  444  orbi1d  763  stbid  800  dcbid  806  pm4.14dc  858  orbididc  920  3orbi123d  1272  3anbi123d  1273  xorbi2d  1341  xorbi1d  1342  nfbidf  1502  drnf1  1694  drnf2  1695  drsb1  1753  sbal2  1973  eubidh  1981  eubid  1982  mobidh  2009  mobid  2010  eqeq1  2122  eqeq2  2125  eleq1w  2176  eleq2w  2177  eleq1  2178  eleq2  2179  nfceqdf  2255  drnfc1  2273  drnfc2  2274  neeq1  2296  neeq2  2297  neleq1  2382  neleq2  2383  dfrex2dc  2403  ralbida  2406  rexbida  2407  ralbidv2  2414  rexbidv2  2415  r19.21t  2482  r19.23t  2514  reubida  2587  rmobida  2592  raleqf  2597  rexeqf  2598  reueq1f  2599  rmoeq1f  2600  cbvraldva2  2633  cbvrexdva2  2634  dfsbcq  2882  sbcbi2  2929  sbcbid  2936  eqsbc3r  2939  sbcabel  2960  sbnfc2  3028  ssconb  3177  uneq1  3191  ineq1  3238  difin2  3306  reuun2  3327  reldisj  3382  undif4  3393  disjssun  3394  sbcssg  3440  eltpg  3537  raltpg  3544  rextpg  3545  r19.12sn  3557  opeq1  3673  opeq2  3674  intmin4  3767  dfiun2g  3813  iindif2m  3848  iinin2m  3849  breq  3899  breq1  3900  breq2  3901  treq  4000  opthg2  4129  poeq1  4189  soeq1  4205  frforeq1  4233  freq1  4234  frforeq2  4235  freq2  4236  frforeq3  4237  weeq1  4246  weeq2  4247  ordeq  4262  limeq  4267  rabxfrd  4358  iunpw  4369  opthprc  4558  releq  4589  sbcrel  4593  eqrel  4596  eqrelrel  4608  xpiindim  4644  brcnvg  4688  brresg  4795  resieq  4797  xpcanm  4946  xpcan2m  4947  dmsnopg  4978  dfco2a  5007  cnvpom  5049  cnvsom  5050  iotaeq  5064  sniota  5083  sbcfung  5115  fneq1  5179  fneq2  5180  feq1  5223  feq2  5224  feq3  5225  sbcfng  5238  sbcfg  5239  f1eq1  5291  f1eq2  5292  f1eq3  5293  foeq1  5309  foeq2  5310  foeq3  5311  f1oeq1  5324  f1oeq2  5325  f1oeq3  5326  fun11iun  5354  mpteqb  5477  dffo3  5533  fmptco  5552  dff13  5635  f1imaeq  5642  f1eqcocnv  5658  fliftcnv  5662  isoeq1  5668  isoeq2  5669  isoeq3  5670  isoeq4  5671  isoeq5  5672  isocnv2  5679  acexmid  5739  fnotovb  5780  mpoeq123  5796  ottposg  6118  dmtpos  6119  smoeq  6153  nnacan  6374  nnmcan  6381  ereq1  6402  ereq2  6403  elecg  6433  ereldm  6438  ixpiinm  6584  enfi  6733  elfi2  6826  fipwssg  6833  ctssdccl  6962  creur  8674  eqreznegel  9355  ltxr  9502  icoshftf1o  9714  elfzm11  9811  elfzomelpfzo  9948  nn0ennn  10146  nnesq  10351  rexfiuz  10701  cau4  10828  sumeq2  11068  fisumcom2  11147  dvdsflip  11445  divgcdcoprm0  11678  hashdvds  11792  tpspropd  12098  tgss2  12143  lmbr2  12278  txcnmpt  12337  txhmeo  12383  blininf  12488  blres  12498  xmeterval  12499  xmspropd  12541  mspropd  12542  metequiv  12559  xmetxpbl  12572  limcdifap  12683  cbvrald  12806
  Copyright terms: Public domain W3C validator