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

Theorem anbi2i 430
Description: Introduce a left 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
anbi2i ((χ φ) ↔ (χ ψ))

Proof of Theorem anbi2i
StepHypRef Expression
1 bi.aa . . 3 (φψ)
21a1i 9 . 2 (χ → (φψ))
32pm5.32i 427 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:  anbi12i  433  mpan10  443  an4  520  an42  521  anandir  525  dcim  783  19.27h  1449  19.27  1450  19.41  1573  sbcof2  1688  sbidm  1728  sb6  1763  3exdistr  1789  4exdistr  1790  2sb5  1856  2sb5rf  1862  sbel2x  1871  eu2  1941  euan  1953  sbmo  1956  mo4f  1957  eu4  1959  moanim  1971  2eu4  1990  clelab  2159  nonconne  2212  r2exf  2336  ceqsex3v  2590  ceqsex4v  2591  ceqsex8v  2593  reu2  2723  reu6  2724  reu4  2729  reu7  2730  2rmorex  2739  rmo3  2843  dfpss2  3023  raldifb  3077  inass  3141  ssddif  3165  difin  3168  invdif  3173  indif  3174  indi  3178  difundi  3183  difindiss  3185  inssdif0im  3285  unipr  3585  uniun  3590  uniin  3591  iunin2  3711  iindif2m  3715  iinin2m  3716  unidif0  3911  mss  3953  eqvinop  3971  opcom  3978  opeqsn  3980  uniuni  4149  zfinf2  4255  elnn  4271  fconstmpt  4330  opeliunxp  4338  xpundi  4339  elvvv  4346  xpiindim  4416  elcnv2  4456  cnvuni  4464  dmuni  4488  opelres  4560  elima3  4618  imai  4624  imainss  4682  ssrnres  4706  cnvresima  4753  mptpreima  4757  coundir  4766  rnco  4770  coass  4782  relrelss  4787  dffun2  4855  dffun4  4856  dffun6f  4858  dffun4f  4861  dffun7  4871  dffun8  4872  dffun9  4873  svrelfun  4907  fncnv  4908  funcnvuni  4911  dfmpt3  4964  fintm  5018  fin  5019  dff12  5034  fores  5058  dff1o4  5077  eqfnfv3  5210  unpreima  5235  ffnfvf  5267  dff13f  5352  ffnov  5547  eqfnov  5549  foov  5589  opabex3d  5690  opabex3  5691  mpt2xopovel  5797  tpostpos  5820  dfsmo2  5843  erinxp  6116  xpassen  6240  distrnqg  6371  subhalfnqq  6397  enq0enq  6413  enq0sym  6414  enq0tr  6416  addnq0mo  6429  mulnq0mo  6430  distrnq0  6441  prarloc  6485  nqprrnd  6525  ltexprlemopl  6574  ltexprlemlol  6575  ltexprlemopu  6576  ltexprlemupu  6577  ltexprlemdisj  6579  ltexprlemloc  6580  recexprlemdisj  6601  addsrmo  6651  mulsrmo  6652  opelreal  6706  elnnz  8011  elznn0nn  8015  zltlen  8075  peano2uz2  8101  peano5uzti  8102  elfzuzb  8634  4fvwrd4  8747  fzind2  8845
  Copyright terms: Public domain W3C validator