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

Theorem 3bitr4g 221
Description: More general version of 3bitr4i 210. 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 190 . 2 (𝜑 → (𝜃𝜒))
4 3bitr4g.3 . 2 (𝜏𝜒)
53, 4syl6bbr 196 1 (𝜑 → (𝜃𝜏))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  bibi1d  231  pm5.32rd  439  orbi1d  738  stbid  775  dcbid  784  pm4.14dc  823  orbididc  897  3orbi123d  1245  3anbi123d  1246  xorbi2d  1314  xorbi1d  1315  nfbidf  1475  drnf1  1665  drnf2  1666  drsb1  1724  sbal2  1943  eubidh  1951  eubid  1952  mobidh  1979  mobid  1980  eqeq1  2091  eqeq2  2094  eleq1w  2145  eleq2w  2146  eleq1  2147  eleq2  2148  nfceqdf  2224  drnfc1  2241  drnfc2  2242  neeq1  2264  neeq2  2265  neleq1  2350  neleq2  2351  dfrex2dc  2367  ralbida  2370  rexbida  2371  ralbidv2  2378  rexbidv2  2379  r19.21t  2444  r19.23t  2475  reubida  2544  rmobida  2549  raleqf  2554  rexeqf  2555  reueq1f  2556  rmoeq1f  2557  cbvraldva2  2590  cbvrexdva2  2591  dfsbcq  2831  sbcbi2  2878  sbcbid  2885  eqsbc3r  2888  sbcabel  2909  sbnfc2  2977  ssconb  3122  uneq1  3136  ineq1  3183  difin2  3250  reuun2  3271  reldisj  3322  undif4  3333  disjssun  3334  sbcssg  3378  eltpg  3471  raltpg  3478  rextpg  3479  r19.12sn  3491  opeq1  3605  opeq2  3606  intmin4  3699  dfiun2g  3745  iindif2m  3780  iinin2m  3781  breq  3822  breq1  3823  breq2  3824  treq  3917  opthg2  4040  poeq1  4100  soeq1  4116  frforeq1  4144  freq1  4145  frforeq2  4146  freq2  4147  frforeq3  4148  weeq1  4157  weeq2  4158  ordeq  4173  limeq  4178  rabxfrd  4265  iunpw  4275  opthprc  4457  releq  4488  sbcrel  4492  eqrel  4495  eqrelrel  4507  xpiindim  4541  brcnvg  4585  brresg  4689  resieq  4691  xpcanm  4836  xpcan2m  4837  dmsnopg  4868  dfco2a  4897  cnvpom  4939  cnvsom  4940  iotaeq  4954  sniota  4973  sbcfung  5004  fneq1  5067  fneq2  5068  feq1  5110  feq2  5111  feq3  5112  sbcfng  5124  sbcfg  5125  f1eq1  5174  f1eq2  5175  f1eq3  5176  foeq1  5192  foeq2  5193  foeq3  5194  f1oeq1  5207  f1oeq2  5208  f1oeq3  5209  fun11iun  5237  mpteqb  5356  dffo3  5409  fmptco  5427  dff13  5508  f1imaeq  5515  f1eqcocnv  5531  fliftcnv  5535  isoeq1  5541  isoeq2  5542  isoeq3  5543  isoeq4  5544  isoeq5  5545  isocnv2  5552  acexmid  5612  fnotovb  5649  mpt2eq123  5665  ottposg  5974  dmtpos  5975  smoeq  6009  nnacan  6223  nnmcan  6230  ereq1  6251  ereq2  6252  elecg  6282  ereldm  6287  enfi  6541  creur  8354  eqreznegel  9031  ltxr  9178  icoshftf1o  9340  elfzm11  9435  elfzomelpfzo  9570  nn0ennn  9768  nnesq  9969  rexfiuz  10317  cau4  10444  sumeq2  10638  dvdsflip  10727  divgcdcoprm0  10958  hashdvds  11072  cbvrald  11126  bj-dcbi  11257
  Copyright terms: Public domain W3C validator