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

Theorem anbi1i 458
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 455 1 ((𝜑𝜒) ↔ (𝜓𝜒))
Colors of variables: wff set class
Syntax hints:  wa 104  wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  anbi2ci  459  anbi12i  460  bianassc  470  an12  561  anandi  590  pm5.53  802  pm5.75  962  3ancoma  985  3ioran  993  an6  1321  19.26-3an  1483  19.28h  1562  19.28  1563  eeeanv  1933  sb3an  1958  moanim  2100  nfrexdya  2513  r19.26-3  2607  r19.41  2632  rexcomf  2639  3reeanv  2647  cbvreu  2701  ceqsex3v  2779  rexab  2899  rexrab  2900  rmo4  2930  rmo3f  2934  reuind  2942  sbc3an  3024  rmo3  3054  ssrab  3233  rexun  3315  elin3  3326  inass  3345  unssdif  3370  indifdir  3391  difin2  3397  inrab2  3408  rabun2  3414  reuun2  3418  undif4  3485  rexdifpr  3619  rexsns  3630  rexdifsn  3723  2ralunsn  3796  iuncom4  3891  iunxiun  3965  inuni  4152  unidif0  4164  bnd2  4170  otth2  4237  copsexg  4240  copsex4g  4243  opeqsn  4248  opelopabsbALT  4255  elpwpwel  4471  suc11g  4552  rabxp  4659  opeliunxp  4677  xpundir  4679  xpiundi  4680  xpiundir  4681  brinxp2  4689  rexiunxp  4764  brres  4908  brresg  4910  dmres  4923  resiexg  4947  dminss  5038  imainss  5039  ssrnres  5066  elxp4  5111  elxp5  5112  cnvresima  5113  coundi  5125  resco  5128  imaco  5129  coiun  5133  coi1  5139  coass  5142  xpcom  5170  dffun2  5221  fncnv  5277  imadiflem  5290  imadif  5291  imainlem  5292  mptun  5342  fcnvres  5394  dff1o2  5461  dff1o3  5462  ffoss  5488  f11o  5489  brprcneu  5503  fvun2  5578  eqfnfv3  5610  respreima  5639  f1ompt  5662  fsn  5683  abrexco  5753  imaiun  5754  f1mpt  5765  dff1o6  5770  oprabid  5900  dfoprab2  5915  oprab4  5939  mpomptx  5959  opabex3d  6115  opabex3  6116  abexssex  6119  dfopab2  6183  dfoprab3s  6184  1stconst  6215  2ndconst  6216  xporderlem  6225  spc2ed  6227  f1od2  6229  brtpos2  6245  tpostpos  6258  tposmpo  6275  oviec  6634  mapsncnv  6688  dfixp  6693  domen  6744  mapsnen  6804  xpsnen  6814  xpcomco  6819  xpassen  6823  ltexpi  7314  dfmq0qs  7406  dfplq0qs  7407  enq0enq  7408  enq0ref  7410  enq0tr  7411  nqnq0pi  7415  prnmaxl  7465  prnminu  7466  suplocexprlemloc  7698  addsrpr  7722  mulsrpr  7723  suplocsrlemb  7783  addcnsr  7811  mulcnsr  7812  ltresr  7816  addvalex  7821  axprecex  7857  elnnz  9239  fnn0ind  9345  rexuz2  9557  qreccl  9618  rexrp  9650  elixx3g  9875  elfz2  9989  elfzuzb  9992  fznn  10062  elfz2nn0  10085  fznn0  10086  4fvwrd4  10113  elfzo2  10123  fzind2  10212  cvg1nlemres  10965  fsum2dlemstep  11413  modfsummod  11437  fprodseq  11562  divalgb  11900  bezoutlemmain  11969  isprm2  12087  oddpwdc  12144  ntreq0  13265  cnnei  13365  txlm  13412  blres  13567  isms2  13587  dedekindicclemicc  13743  limcrcl  13760  bdcriota  14257  bj-peano4  14329  alsconv  14448
  Copyright terms: Public domain W3C validator