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  780  stbid  817  dcbid  823  pm4.14dc  875  orbididc  937  3orbi123d  1289  3anbi123d  1290  xorbi2d  1358  xorbi1d  1359  nfbidf  1519  drnf1  1711  drnf2  1712  drsb1  1771  sbal2  1997  eubidh  2005  eubid  2006  mobidh  2033  mobid  2034  eqeq1  2146  eqeq2  2149  eleq1w  2200  eleq2w  2201  eleq1  2202  eleq2  2203  nfceqdf  2280  drnfc1  2298  drnfc2  2299  neeq1  2321  neeq2  2322  neleq1  2407  neleq2  2408  dfrex2dc  2428  ralbida  2431  rexbida  2432  ralbidv2  2439  rexbidv2  2440  r19.21t  2507  r19.23t  2539  reubida  2612  rmobida  2617  raleqf  2622  rexeqf  2623  reueq1f  2624  rmoeq1f  2625  cbvraldva2  2661  cbvrexdva2  2662  dfsbcq  2911  sbcbi2  2959  sbcbid  2966  eqsbc3r  2969  sbcabel  2990  sbnfc2  3060  ssconb  3209  uneq1  3223  ineq1  3270  difin2  3338  reuun2  3359  reldisj  3414  undif4  3425  disjssun  3426  sbcssg  3472  eltpg  3569  raltpg  3576  rextpg  3577  r19.12sn  3589  opeq1  3705  opeq2  3706  intmin4  3799  dfiun2g  3845  iindif2m  3880  iinin2m  3881  breq  3931  breq1  3932  breq2  3933  treq  4032  opthg2  4161  poeq1  4221  soeq1  4237  frforeq1  4265  freq1  4266  frforeq2  4267  freq2  4268  frforeq3  4269  weeq1  4278  weeq2  4279  ordeq  4294  limeq  4299  rabxfrd  4390  iunpw  4401  opthprc  4590  releq  4621  sbcrel  4625  eqrel  4628  eqrelrel  4640  xpiindim  4676  brcnvg  4720  brresg  4827  resieq  4829  xpcanm  4978  xpcan2m  4979  dmsnopg  5010  dfco2a  5039  cnvpom  5081  cnvsom  5082  iotaeq  5096  sniota  5115  sbcfung  5147  fneq1  5211  fneq2  5212  feq1  5255  feq2  5256  feq3  5257  sbcfng  5270  sbcfg  5271  f1eq1  5323  f1eq2  5324  f1eq3  5325  foeq1  5341  foeq2  5342  foeq3  5343  f1oeq1  5356  f1oeq2  5357  f1oeq3  5358  fun11iun  5388  mpteqb  5511  dffo3  5567  fmptco  5586  dff13  5669  f1imaeq  5676  f1eqcocnv  5692  fliftcnv  5696  isoeq1  5702  isoeq2  5703  isoeq3  5704  isoeq4  5705  isoeq5  5706  isocnv2  5713  acexmid  5773  fnotovb  5814  mpoeq123  5830  ottposg  6152  dmtpos  6153  smoeq  6187  nnacan  6408  nnmcan  6415  ereq1  6436  ereq2  6437  elecg  6467  ereldm  6472  ixpiinm  6618  enfi  6767  elfi2  6860  fipwssg  6867  ctssdccl  6996  creur  8729  eqreznegel  9418  ltxr  9574  icoshftf1o  9786  elfzm11  9883  elfzomelpfzo  10020  nn0ennn  10218  nnesq  10423  rexfiuz  10773  cau4  10900  sumeq2  11140  fisumcom2  11219  dvdsflip  11560  divgcdcoprm0  11793  hashdvds  11908  tpspropd  12217  tgss2  12262  lmbr2  12397  txcnmpt  12456  txhmeo  12502  blininf  12607  blres  12617  xmeterval  12618  xmspropd  12660  mspropd  12661  metequiv  12678  xmetxpbl  12691  limcdifap  12814  cbvrald  13054
  Copyright terms: Public domain W3C validator