ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  anbi2i 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  784  19.27h  1452  19.27  1453  19.41  1576  sbcof2  1691  sbidm  1731  sb6  1766  3exdistr  1792  4exdistr  1793  2sb5  1859  2sb5rf  1865  sbel2x  1874  eu2  1944  euan  1956  sbmo  1959  mo4f  1960  eu4  1962  moanim  1974  2eu4  1993  clelab  2162  nonconne  2217  r2exf  2342  ceqsex3v  2596  ceqsex4v  2597  ceqsex8v  2599  reu2  2729  reu6  2730  reu4  2735  reu7  2736  2rmorex  2745  rmo3  2849  dfpss2  3029  raldifb  3083  inass  3147  ssddif  3171  difin  3174  invdif  3179  indif  3180  indi  3184  difundi  3189  difindiss  3191  inssdif0im  3291  unipr  3594  uniun  3599  uniin  3600  iunin2  3720  iindif2m  3724  iinin2m  3725  unidif0  3920  mss  3962  eqvinop  3980  opcom  3987  opeqsn  3989  uniuni  4183  zfinf2  4312  elnn  4328  fconstmpt  4387  opeliunxp  4395  xpundi  4396  elvvv  4403  xpiindim  4473  elcnv2  4513  cnvuni  4521  dmuni  4545  opelres  4617  elima3  4675  imai  4681  imainss  4739  ssrnres  4763  cnvresima  4810  mptpreima  4814  coundir  4823  rnco  4827  coass  4839  relrelss  4844  dffun2  4912  dffun4  4913  dffun6f  4915  dffun4f  4918  dffun7  4928  dffun8  4929  dffun9  4930  svrelfun  4964  fncnv  4965  funcnvuni  4968  dfmpt3  5021  fintm  5075  fin  5076  dff12  5091  fores  5115  dff1o4  5134  eqfnfv3  5267  unpreima  5292  ffnfvf  5324  dff13f  5409  ffnov  5605  eqfnov  5607  foov  5647  opabex3d  5748  opabex3  5749  mpt2xopovel  5856  tpostpos  5879  dfsmo2  5902  erinxp  6180  xpassen  6304  distrnqg  6483  subhalfnqq  6510  enq0enq  6527  enq0sym  6528  enq0tr  6530  addnq0mo  6543  mulnq0mo  6544  distrnq0  6555  prarloc  6599  nqprrnd  6639  ltexprlemopl  6697  ltexprlemlol  6698  ltexprlemopu  6699  ltexprlemupu  6700  ltexprlemdisj  6702  ltexprlemloc  6703  recexprlemdisj  6726  caucvgprprlemell  6781  caucvgprprlemelu  6782  addsrmo  6826  mulsrmo  6827  opelreal  6902  axcaucvglemres  6971  elnnz  8253  elznn0nn  8257  zltlen  8317  peano2uz2  8343  peano5uzti  8344  qltlen  8573  elfzuzb  8882  4fvwrd4  8995  fzind2  9093  cvg1nlemres  9558
  Copyright terms: Public domain W3C validator