ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  anbi1i Unicode version

Theorem anbi1i 446
Description: Introduce a right conjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)
Hypothesis
Ref Expression
bi.aa  |-  ( ph  <->  ps )
Assertion
Ref Expression
anbi1i  |-  ( (
ph  /\  ch )  <->  ( ps  /\  ch )
)

Proof of Theorem anbi1i
StepHypRef Expression
1 bi.aa . . 3  |-  ( ph  <->  ps )
21a1i 9 . 2  |-  ( ch 
->  ( ph  <->  ps )
)
32pm5.32ri 443 1  |-  ( (
ph  /\  ch )  <->  ( ps  /\  ch )
)
Colors of variables: wff set class
Syntax hints:    /\ wa 102    <-> 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:  anbi2ci  447  anbi12i  448  an12  528  anandi  557  pm5.53  751  pm5.75  908  3ancoma  931  3ioran  939  an6  1257  19.26-3an  1417  19.28h  1499  19.28  1500  eeeanv  1856  sb3an  1880  moanim  2022  nfrexdya  2413  r19.26-3  2499  r19.41  2522  rexcomf  2529  3reeanv  2537  cbvreu  2588  ceqsex3v  2661  rexab  2775  rexrab  2776  rmo4  2806  rmo3f  2810  reuind  2818  sbc3an  2898  rmo3  2928  ssrab  3097  rexun  3178  elin3  3189  inass  3208  unssdif  3232  indifdir  3253  difin2  3259  inrab2  3270  rabun2  3276  reuun2  3280  undif4  3342  rexsns  3477  rexdifsn  3567  2ralunsn  3637  iuncom4  3732  iunxiun  3805  inuni  3983  unidif0  3994  bnd2  4000  otth2  4059  copsexg  4062  copsex4g  4065  opeqsn  4070  opelopabsbALT  4077  suc11g  4363  rabxp  4463  opeliunxp  4481  xpundir  4483  xpiundi  4484  xpiundir  4485  brinxp2  4493  rexiunxp  4566  brres  4707  brresg  4709  dmres  4721  resiexg  4744  dminss  4833  imainss  4834  ssrnres  4860  elxp4  4905  elxp5  4906  cnvresima  4907  coundi  4919  resco  4922  imaco  4923  coiun  4927  coi1  4933  coass  4936  xpcom  4964  dffun2  5012  fncnv  5066  imadiflem  5079  imadif  5080  imainlem  5081  mptun  5130  fcnvres  5178  dff1o2  5242  dff1o3  5243  ffoss  5269  f11o  5270  brprcneu  5282  fvun2  5355  eqfnfv3  5383  respreima  5411  f1ompt  5434  fsn  5453  abrexco  5520  imaiun  5521  f1mpt  5532  dff1o6  5537  oprabid  5663  dfoprab2  5678  oprab4  5701  mpt2mptx  5721  opabex3d  5874  opabex3  5875  abexssex  5878  dfopab2  5941  dfoprab3s  5942  1stconst  5968  2ndconst  5969  xporderlem  5978  spc2ed  5980  f1od2  5982  brtpos2  5998  tpostpos  6011  tposmpt2  6028  oviec  6378  mapsncnv  6432  domen  6448  mapsnen  6508  xpsnen  6517  xpcomco  6522  xpassen  6526  ltexpi  6875  dfmq0qs  6967  dfplq0qs  6968  enq0enq  6969  enq0ref  6971  enq0tr  6972  nqnq0pi  6976  prnmaxl  7026  prnminu  7027  addsrpr  7270  mulsrpr  7271  addcnsr  7350  mulcnsr  7351  ltresr  7355  addvalex  7360  axprecex  7394  elnnz  8730  fnn0ind  8832  rexuz2  9038  qreccl  9096  rexrp  9125  elixx3g  9288  elfz2  9400  elfzuzb  9403  fznn  9470  elfz2nn0  9493  fznn0  9494  4fvwrd4  9516  elfzo2  9526  fzind2  9615  cvg1nlemres  10383  fsum2dlemstep  10791  modfsummod  10815  divalgb  11018  bezoutlemmain  11080  isprm2  11192  oddpwdc  11245  bdcriota  11431  bj-peano4  11507  alsconv  11580
  Copyright terms: Public domain W3C validator