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

Theorem anbi2i 450
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 447 1 ((𝜒𝜑) ↔ (𝜒𝜓))
Colors of variables: wff set class
Syntax hints:  wa 103  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  anbi12i  453  mpan10  463  an4  558  an42  559  anandir  563  dcim  809  19.27h  1522  19.27  1523  19.41  1647  sbcof2  1764  sbidm  1805  sb6  1840  3exdistr  1867  4exdistr  1868  2sb5  1934  2sb5rf  1940  sbel2x  1949  eu2  2019  euan  2031  sbmo  2034  mo4f  2035  eu4  2037  moanim  2049  2eu4  2068  clelab  2240  nonconne  2295  r2exf  2428  ceqsex3v  2700  ceqsex4v  2701  ceqsex8v  2703  reu2  2843  reu6  2844  reu4  2849  reu7  2850  rmo3f  2852  rmo4f  2853  2rmorex  2861  rmo3  2970  raldifb  3184  inass  3254  dfss4st  3277  ssddif  3278  difin  3281  invdif  3286  indif  3287  indi  3291  difundi  3296  difindiss  3298  inssdif0im  3398  ssdifsn  3619  unipr  3718  uniun  3723  uniin  3724  iunin2  3844  iindif2m  3848  iinin2m  3849  elpwpw  3867  unidif0  4059  mss  4116  eqvinop  4133  opcom  4140  opeqsn  4142  uniuni  4340  zfinf2  4471  elnn  4487  fconstmpt  4554  opeliunxp  4562  xpundi  4563  elvvv  4570  xpiindim  4644  elcnv2  4685  cnvuni  4693  dmuni  4717  opelres  4792  elima3  4856  imai  4863  imainss  4922  ssrnres  4949  cnvresima  4996  mptpreima  5000  coundir  5009  rnco  5013  coass  5025  relrelss  5033  dffun2  5101  dffun4  5102  dffun6f  5104  dffun4f  5107  dffun7  5118  dffun8  5119  dffun9  5120  svrelfun  5156  fncnv  5157  funcnvuni  5160  dfmpt3  5213  fintm  5276  fin  5277  dff12  5295  fores  5322  dff1o4  5341  eqfnfv3  5486  unpreima  5511  ffnfvf  5545  dff13f  5637  ffnov  5841  eqfnov  5843  foov  5883  opabex3d  5985  opabex3  5986  mpoxopovel  6104  tpostpos  6127  dfsmo2  6150  tfr1onlemaccex  6211  tfrcllembxssdm  6219  tfrcllemaccex  6224  tfrcllemres  6225  tfrcldm  6226  erinxp  6469  mapsncnv  6555  cbvixp  6575  ixpin  6583  ixpiinm  6584  mptelixpg  6594  elixpsn  6595  ixpsnf1o  6596  mapsnen  6671  xpassen  6690  distrnqg  7159  subhalfnqq  7186  enq0enq  7203  enq0sym  7204  enq0tr  7206  addnq0mo  7219  mulnq0mo  7220  distrnq0  7231  prarloc  7275  nqprrnd  7315  ltexprlemopl  7373  ltexprlemlol  7374  ltexprlemopu  7375  ltexprlemupu  7376  ltexprlemdisj  7378  ltexprlemloc  7379  recexprlemdisj  7402  caucvgprprlemell  7457  caucvgprprlemelu  7458  addsrmo  7515  mulsrmo  7516  opelreal  7599  axcaucvglemres  7671  axpre-suploc  7674  elnnz  9015  elznn0nn  9019  zltlen  9080  suprzclex  9100  peano2uz2  9109  peano5uzti  9110  qltlen  9381  elfzuzb  9740  4fvwrd4  9857  fzind2  9956  cvg1nlemres  10697  rexfiuz  10701  cbvsum  11069  mertenslem2  11245  mertensabs  11246  ndvdssub  11523  isprm2  11694  isprm4  11696  hashdvds  11792  isbasis2g  12107  tgval2  12115  elcncf1di  12630
  Copyright terms: Public domain W3C validator