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

Theorem anbi1i 434
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 431 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  435  anbi12i  436  an12  483  anandi  511  pm5.53  702  pm5.75  857  3ancoma  880  3ioran  888  an6  1201  19.26-3an  1352  19.28h  1436  19.28  1437  eeeanv  1790  sb3an  1814  moanim  1956  nfrexdya  2337  r19.26-3  2421  r19.41  2443  rexcomf  2450  3reeanv  2458  cbvreu  2509  ceqsex3v  2573  rexab  2680  rexrab  2681  rmo4  2711  reuind  2721  rmo3  2826  ssrab  2995  rexun  3100  elin3  3105  inass  3124  unssdif  3149  indifdir  3170  difin2  3176  inrab2  3187  rabun2  3193  reuun2  3197  undif4  3261  rexsns  3383  rexsnsOLD  3384  rexdifsn  3473  2ralunsn  3543  iuncom4  3638  iunxiun  3710  inuni  3883  unidif0  3894  bnd2  3900  otth2  3952  copsexg  3955  copsex4g  3958  opeqsn  3963  opelopabsbALT  3970  suc11g  4219  rabxp  4307  opeliunxp  4322  xpundir  4324  xpiundi  4325  xpiundir  4326  brinxp2  4334  rexiunxp  4405  brres  4545  brresg  4547  dmres  4559  resiexg  4580  dminss  4665  imainss  4666  ssrnres  4690  elxp4  4735  elxp5  4736  cnvresima  4737  coundi  4749  resco  4752  imaco  4753  coiun  4757  coi1  4763  coass  4766  xpcom  4791  dffun2  4839  fncnv  4891  imadiflem  4904  imadif  4905  imainlem  4906  mptun  4955  fcnvres  4998  dff1o2  5056  dff1o3  5057  ffoss  5083  f11o  5084  brprcneu  5096  fvun2  5165  eqfnfv3  5192  respreima  5220  f1ompt  5245  fsn  5260  abrexco  5323  imaiun  5324  f1mpt  5335  dff1o6  5341  oprabid  5461  dfoprab2  5475  oprab4  5498  mpt2mptx  5518  opabex3d  5671  opabex3  5672  abexssex  5675  dfopab2  5738  dfoprab3s  5739  1stconst  5765  2ndconst  5766  xporderlem  5774  brtpos2  5788  tpostpos  5801  tposmpt2  5818  oviec  6123  ltexpi  6197  dfmq0qs  6284  dfplq0qs  6285  enq0enq  6286  enq0ref  6288  enq0tr  6289  nqnq0pi  6293  prnmaxl  6342  prnminu  6343  addsrpr  6492  mulsrpr  6493  addcnsr  6545  mulcnsr  6546  ltresr  6550  axprecex  6574  bdcriota  7110  bj-peano4  7177  alsconv  7211
  Copyright terms: Public domain W3C validator