ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  anbi1i GIF 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 (𝜑𝜓)
Assertion
Ref Expression
anbi1i ((𝜑𝜒) ↔ (𝜓𝜒))

Proof of Theorem anbi1i
StepHypRef Expression
1 bi.aa . . 3 (𝜑𝜓)
21a1i 9 . 2 (𝜒 → (𝜑𝜓))
32pm5.32ri 443 1 ((𝜑𝜒) ↔ (𝜓𝜒))
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  526  anandi  555  pm5.53  749  pm5.75  906  3ancoma  929  3ioran  937  an6  1255  19.26-3an  1415  19.28h  1497  19.28  1498  eeeanv  1853  sb3an  1877  moanim  2019  nfrexdya  2409  r19.26-3  2495  r19.41  2518  rexcomf  2525  3reeanv  2533  cbvreu  2584  ceqsex3v  2655  rexab  2768  rexrab  2769  rmo4  2799  reuind  2809  sbc3an  2889  rmo3  2919  ssrab  3088  rexun  3169  elin3  3180  inass  3199  unssdif  3223  indifdir  3244  difin2  3250  inrab2  3261  rabun2  3267  reuun2  3271  undif4  3333  rexsns  3465  rexdifsn  3555  2ralunsn  3625  iuncom4  3720  iunxiun  3792  inuni  3966  unidif0  3977  bnd2  3983  otth2  4042  copsexg  4045  copsex4g  4048  opeqsn  4053  opelopabsbALT  4060  suc11g  4346  rabxp  4446  opeliunxp  4461  xpundir  4463  xpiundi  4464  xpiundir  4465  brinxp2  4473  rexiunxp  4546  brres  4687  brresg  4689  dmres  4701  resiexg  4724  dminss  4812  imainss  4813  ssrnres  4839  elxp4  4884  elxp5  4885  cnvresima  4886  coundi  4898  resco  4901  imaco  4902  coiun  4906  coi1  4912  coass  4915  xpcom  4943  dffun2  4991  fncnv  5045  imadiflem  5058  imadif  5059  imainlem  5060  mptun  5109  fcnvres  5157  dff1o2  5221  dff1o3  5222  ffoss  5248  f11o  5249  brprcneu  5261  fvun2  5334  eqfnfv3  5362  respreima  5390  f1ompt  5413  fsn  5432  abrexco  5499  imaiun  5500  f1mpt  5511  dff1o6  5516  oprabid  5638  dfoprab2  5653  oprab4  5676  mpt2mptx  5696  opabex3d  5849  opabex3  5850  abexssex  5853  dfopab2  5916  dfoprab3s  5917  1stconst  5943  2ndconst  5944  xporderlem  5953  spc2ed  5955  f1od2  5957  brtpos2  5970  tpostpos  5983  tposmpt2  6000  oviec  6350  mapsncnv  6404  domen  6420  mapsnen  6480  xpsnen  6489  xpcomco  6494  xpassen  6498  ltexpi  6840  dfmq0qs  6932  dfplq0qs  6933  enq0enq  6934  enq0ref  6936  enq0tr  6937  nqnq0pi  6941  prnmaxl  6991  prnminu  6992  addsrpr  7235  mulsrpr  7236  addcnsr  7315  mulcnsr  7316  ltresr  7320  addvalex  7325  axprecex  7359  elnnz  8693  fnn0ind  8795  rexuz2  9001  qreccl  9059  rexrp  9088  elixx3g  9251  elfz2  9363  elfzuzb  9366  fznn  9433  elfz2nn0  9456  fznn0  9457  4fvwrd4  9479  elfzo2  9489  fzind2  9578  cvg1nlemres  10313  divalgb  10800  bezoutlemmain  10862  isprm2  10974  oddpwdc  11027  bdcriota  11212  bj-peano4  11288  alsconv  11359
  Copyright terms: Public domain W3C validator