ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3bitr4g Unicode 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  |-  ( ph  ->  ( ps  <->  ch )
)
3bitr4g.2  |-  ( th  <->  ps )
3bitr4g.3  |-  ( ta  <->  ch )
Assertion
Ref Expression
3bitr4g  |-  ( ph  ->  ( th  <->  ta )
)

Proof of Theorem 3bitr4g
StepHypRef Expression
1 3bitr4g.2 . . 3  |-  ( th  <->  ps )
2 3bitr4g.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2syl5bb 191 . 2  |-  ( ph  ->  ( th  <->  ch )
)
4 3bitr4g.3 . 2  |-  ( ta  <->  ch )
53, 4syl6bbr 197 1  |-  ( ph  ->  ( th  <->  ta )
)
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  446  orbi1d  765  stbid  802  dcbid  808  pm4.14dc  860  orbididc  922  3orbi123d  1274  3anbi123d  1275  xorbi2d  1343  xorbi1d  1344  nfbidf  1504  drnf1  1696  drnf2  1697  drsb1  1755  sbal2  1975  eubidh  1983  eubid  1984  mobidh  2011  mobid  2012  eqeq1  2124  eqeq2  2127  eleq1w  2178  eleq2w  2179  eleq1  2180  eleq2  2181  nfceqdf  2257  drnfc1  2275  drnfc2  2276  neeq1  2298  neeq2  2299  neleq1  2384  neleq2  2385  dfrex2dc  2405  ralbida  2408  rexbida  2409  ralbidv2  2416  rexbidv2  2417  r19.21t  2484  r19.23t  2516  reubida  2589  rmobida  2594  raleqf  2599  rexeqf  2600  reueq1f  2601  rmoeq1f  2602  cbvraldva2  2635  cbvrexdva2  2636  dfsbcq  2884  sbcbi2  2931  sbcbid  2938  eqsbc3r  2941  sbcabel  2962  sbnfc2  3030  ssconb  3179  uneq1  3193  ineq1  3240  difin2  3308  reuun2  3329  reldisj  3384  undif4  3395  disjssun  3396  sbcssg  3442  eltpg  3539  raltpg  3546  rextpg  3547  r19.12sn  3559  opeq1  3675  opeq2  3676  intmin4  3769  dfiun2g  3815  iindif2m  3850  iinin2m  3851  breq  3901  breq1  3902  breq2  3903  treq  4002  opthg2  4131  poeq1  4191  soeq1  4207  frforeq1  4235  freq1  4236  frforeq2  4237  freq2  4238  frforeq3  4239  weeq1  4248  weeq2  4249  ordeq  4264  limeq  4269  rabxfrd  4360  iunpw  4371  opthprc  4560  releq  4591  sbcrel  4595  eqrel  4598  eqrelrel  4610  xpiindim  4646  brcnvg  4690  brresg  4797  resieq  4799  xpcanm  4948  xpcan2m  4949  dmsnopg  4980  dfco2a  5009  cnvpom  5051  cnvsom  5052  iotaeq  5066  sniota  5085  sbcfung  5117  fneq1  5181  fneq2  5182  feq1  5225  feq2  5226  feq3  5227  sbcfng  5240  sbcfg  5241  f1eq1  5293  f1eq2  5294  f1eq3  5295  foeq1  5311  foeq2  5312  foeq3  5313  f1oeq1  5326  f1oeq2  5327  f1oeq3  5328  fun11iun  5356  mpteqb  5479  dffo3  5535  fmptco  5554  dff13  5637  f1imaeq  5644  f1eqcocnv  5660  fliftcnv  5664  isoeq1  5670  isoeq2  5671  isoeq3  5672  isoeq4  5673  isoeq5  5674  isocnv2  5681  acexmid  5741  fnotovb  5782  mpoeq123  5798  ottposg  6120  dmtpos  6121  smoeq  6155  nnacan  6376  nnmcan  6383  ereq1  6404  ereq2  6405  elecg  6435  ereldm  6440  ixpiinm  6586  enfi  6735  elfi2  6828  fipwssg  6835  ctssdccl  6964  creur  8681  eqreznegel  9362  ltxr  9517  icoshftf1o  9729  elfzm11  9826  elfzomelpfzo  9963  nn0ennn  10161  nnesq  10366  rexfiuz  10716  cau4  10843  sumeq2  11083  fisumcom2  11162  dvdsflip  11461  divgcdcoprm0  11694  hashdvds  11808  tpspropd  12114  tgss2  12159  lmbr2  12294  txcnmpt  12353  txhmeo  12399  blininf  12504  blres  12514  xmeterval  12515  xmspropd  12557  mspropd  12558  metequiv  12575  xmetxpbl  12588  limcdifap  12711  cbvrald  12891
  Copyright terms: Public domain W3C validator