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

Theorem anbi2i 438
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 435 1 ((𝜒𝜑) ↔ (𝜒𝜓))
Colors of variables: wff set class
Syntax hints:  wa 101  wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  anbi12i  441  mpan10  451  an4  528  an42  529  anandir  533  dcim  795  19.27h  1468  19.27  1469  19.41  1592  sbcof2  1707  sbidm  1747  sb6  1782  3exdistr  1808  4exdistr  1809  2sb5  1875  2sb5rf  1881  sbel2x  1890  eu2  1960  euan  1972  sbmo  1975  mo4f  1976  eu4  1978  moanim  1990  2eu4  2009  clelab  2178  nonconne  2232  r2exf  2359  ceqsex3v  2613  ceqsex4v  2614  ceqsex8v  2616  reu2  2752  reu6  2753  reu4  2758  reu7  2759  2rmorex  2768  rmo3  2877  dfpss2  3057  raldifb  3111  inass  3175  ssddif  3199  difin  3202  invdif  3207  indif  3208  indi  3212  difundi  3217  difindiss  3219  inssdif0im  3319  unipr  3622  uniun  3627  uniin  3628  iunin2  3748  iindif2m  3752  iinin2m  3753  unidif0  3948  mss  3990  eqvinop  4008  opcom  4015  opeqsn  4017  uniuni  4211  zfinf2  4340  elnn  4356  fconstmpt  4415  opeliunxp  4423  xpundi  4424  elvvv  4431  xpiindim  4501  elcnv2  4541  cnvuni  4549  dmuni  4573  opelres  4645  elima3  4703  imai  4709  imainss  4767  ssrnres  4791  cnvresima  4838  mptpreima  4842  coundir  4851  rnco  4855  coass  4867  relrelss  4872  dffun2  4940  dffun4  4941  dffun6f  4943  dffun4f  4946  dffun7  4956  dffun8  4957  dffun9  4958  svrelfun  4992  fncnv  4993  funcnvuni  4996  dfmpt3  5049  fintm  5103  fin  5104  dff12  5119  fores  5143  dff1o4  5162  eqfnfv3  5295  unpreima  5320  ffnfvf  5352  dff13f  5437  ffnov  5633  eqfnov  5635  foov  5675  opabex3d  5776  opabex3  5777  mpt2xopovel  5887  tpostpos  5910  dfsmo2  5933  erinxp  6211  xpassen  6335  distrnqg  6543  subhalfnqq  6570  enq0enq  6587  enq0sym  6588  enq0tr  6590  addnq0mo  6603  mulnq0mo  6604  distrnq0  6615  prarloc  6659  nqprrnd  6699  ltexprlemopl  6757  ltexprlemlol  6758  ltexprlemopu  6759  ltexprlemupu  6760  ltexprlemdisj  6762  ltexprlemloc  6763  recexprlemdisj  6786  caucvgprprlemell  6841  caucvgprprlemelu  6842  addsrmo  6886  mulsrmo  6887  opelreal  6962  axcaucvglemres  7031  elnnz  8312  elznn0nn  8316  zltlen  8377  peano2uz2  8404  peano5uzti  8405  qltlen  8672  elfzuzb  8986  4fvwrd4  9099  fzind2  9197  cvg1nlemres  9812  rexfiuz  9816  ndvdssub  10242
  Copyright terms: Public domain W3C validator