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

Theorem anbi1i 431
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 428 1 ((φ χ) ↔ (ψ χ))
Colors of variables: wff set class
Syntax hints:   wa 97  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  anbi2ci  432  anbi12i  433  an12  480  anandi  509  pm5.53  699  pm5.75  851  3ancoma  874  3ioran  882  an6  1197  19.26-3an  1346  19.28h  1428  19.28  1429  eeeanv  1782  sb3an  1806  moanim  1948  nfrexdya  2329  r19.26-3  2413  r19.41  2435  rexcomf  2442  3reeanv  2450  cbvreu  2501  ceqsex3v  2565  rexab  2672  rexrab  2673  rmo4  2703  reuind  2713  rmo3  2818  ssrab  2987  rexun  3092  elin3  3097  inass  3116  unssdif  3141  indifdir  3162  difin2  3168  inrab2  3179  rabun2  3185  reuun2  3189  undif4  3253  rexsns  3373  rexsnsOLD  3374  rexdifsn  3463  2ralunsn  3533  iuncom4  3628  iunxiun  3700  inuni  3873  unidif0  3884  bnd2  3890  otth2  3942  copsexg  3945  copsex4g  3948  opeqsn  3953  opelopabsbALT  3960  suc11g  4208  rabxp  4296  opeliunxp  4311  xpundir  4313  xpiundi  4314  xpiundir  4315  brinxp2  4323  rexiunxp  4394  brres  4534  brresg  4536  dmres  4548  resiexg  4569  dminss  4654  imainss  4655  ssrnres  4679  elxp4  4724  elxp5  4725  cnvresima  4726  coundi  4738  resco  4741  imaco  4742  coiun  4746  coi1  4752  coass  4755  xpcom  4780  dffun2  4828  fncnv  4880  imadiflem  4893  imadif  4894  imainlem  4895  mptun  4944  fcnvres  4987  dff1o2  5045  dff1o3  5046  ffoss  5072  f11o  5073  brprcneu  5085  fvun2  5154  eqfnfv3  5181  respreima  5209  f1ompt  5234  fsn  5249  abrexco  5312  imaiun  5313  f1mpt  5324  dff1o6  5330  oprabid  5450  dfoprab2  5464  oprab4  5487  mpt2mptx  5507  opabex3d  5660  opabex3  5661  abexssex  5664  dfopab2  5727  dfoprab3s  5728  1stconst  5754  2ndconst  5755  xporderlem  5763  brtpos2  5777  tpostpos  5790  tposmpt2  5807  oviec  6112  ltexpi  6184  dfmq0qs  6271  dfplq0qs  6272  enq0enq  6273  enq0ref  6275  enq0tr  6276  nqnq0pi  6280  prnmaxl  6329  prnminu  6330  addsrpr  6484  mulsrpr  6485  addcnsr  6541  mulcnsr  6542  ltresr  6546  axprecex  6570  elnnz  7830  fnn0ind  7920  qreccl  8059  rexrp  8087  bdcriota  8340  bj-peano4  8411  alsconv  8445
  Copyright terms: Public domain W3C validator