MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imbi1i Structured version   Visualization version   GIF version

Theorem imbi1i 351
Description: Introduce a consequent to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 17-Sep-2013.)
Hypothesis
Ref Expression
imbi1i.1 (𝜑𝜓)
Assertion
Ref Expression
imbi1i ((𝜑𝜒) ↔ (𝜓𝜒))

Proof of Theorem imbi1i
StepHypRef Expression
1 imbi1i.1 . 2 (𝜑𝜓)
2 imbi1 349 . 2 ((𝜑𝜓) → ((𝜑𝜒) ↔ (𝜓𝜒)))
31, 2ax-mp 5 1 ((𝜑𝜒) ↔ (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 208
This theorem is referenced by:  ancomst  465  imor  849  ifpn  1066  eximal  1776  19.43  1876  19.37v  1991  19.37  2227  sbrim  2307  sbor  2310  dfsb3  2531  dfsb3ALT  2590  sbrimALT  2607  mo4f  2649  2mos  2733  neor  3113  r3al  3207  r19.23v  3284  r19.23t  3318  r19.43  3356  ceqsralt  3534  ralab  3688  ralrab  3689  euind  3719  reu2  3720  rmo4  3725  rmo3f  3729  rmo4f  3730  reuind  3748  2reu5lem3  3752  rmo3  3876  rmo3OLD  3877  dfdif3  4095  raldifb  4125  elunant  4158  inssdif0  4333  ssundif  4436  dfif2  4472  pwss  4562  ralsnsg  4605  disjsn  4646  snssg  4716  raldifsni  4727  raldifsnb  4728  unissb  4868  intpr  4907  dfiin2g  4954  disjor  5043  dftr2  5171  axrep1  5188  axrep6  5194  axpweq  5262  zfpow  5264  axpow2  5265  reusv2lem4  5298  reusv2  5300  raliunxp  5709  idrefALT  5972  asymref2  5976  dffun2  6364  dffun4  6366  dffun5  6367  dffun7  6381  fununi  6428  fvn0ssdmfun  6840  dff13  7009  dff14b  7025  zfun  7456  uniex2  7458  dfom2  7575  fimaxg  8759  fiint  8789  dfsup2  8902  fiming  8956  oemapso  9139  scottexs  9310  scott0s  9311  iscard2  9399  acnnum  9472  dfac9  9556  dfacacn  9561  kmlem4  9573  kmlem12  9581  axpowndlem3  10015  zfcndun  10031  zfcndpow  10032  zfcndac  10035  axgroth5  10240  axgroth6  10244  addsrmo  10489  mulsrmo  10490  infm3  11594  raluz2  12291  nnwos  12309  ralrp  12404  cotr2g  14331  lo1resb  14916  rlimresb  14917  o1resb  14918  modfsummod  15144  isprm4  16023  acsfn1  16927  acsfn2  16929  lublecllem  17593  isirred2  19387  isdomn2  20007  iunocv  20760  ist1-2  21890  isnrm2  21901  dfconn2  21962  alexsubALTlem3  22592  ismbl  24061  dyadmbllem  24134  ellimc3  24411  dchrelbas2  25746  dchrelbas3  25747  isch2  28933  choc0  29036  h1dei  29260  mdsl2i  30032  disjorf  30263  bnj1101  31961  bnj1109  31963  bnj1533  32029  bnj580  32090  bnj864  32099  bnj865  32100  bnj978  32126  bnj1049  32149  bnj1090  32154  bnj1145  32168  axextprim  32830  axunprim  32832  axpowprim  32833  untuni  32838  3orit  32848  biimpexp  32849  elintfv  32910  dfon2lem8  32938  soseq  32999  dfom5b  33276  rdgeqoa  34539  wl-equsalcom  34669  wl-dfralflem  34724  poimirlem25  34803  poimirlem30  34808  tsim1  35295  inxpss  35456  idinxpss  35457  idinxpssinxp  35461  ineleq  35495  cocossss  35567  cosscnvssid3  35602  trcoss2  35610  redundpbi1  35752  dfeldisj3  35838  cvlsupr3  36366  pmapglbx  36791  isltrn2N  37142  cdlemefrs29bpre0  37418  fphpd  39297  dford4  39510  fnwe2lem2  39535  isdomn3  39688  ifpidg  39741  ifpid1g  39744  ifpor123g  39758  dfsucon  39773  undmrnresiss  39848  elintima  39882  df3or2  39997  dfhe3  40005  dffrege76  40169  dffrege115  40208  frege131  40224  ntrneikb  40328  ismnuprim  40514  pm14.12  40637  dfvd2an  40800  dfvd3  40809  dfvd3an  40812  uun2221  41031  uun2221p1  41032  uun2221p2  41033  disjinfi  41338  supxrleubrnmptf  41611  fsummulc1f  41735  fsumiunss  41740  fnlimfvre2  41842  limsupreuz  41902  limsupvaluz2  41903  dvmptmulf  42106  dvnmul  42112  dvmptfprodlem  42113  dvnprodlem2  42116  sge0ltfirpmpt2  42593  hoidmv1le  42761  hoidmvle  42767  vonioolem2  42848  smflimlem3  42934  2reu8i  43197  ichexmpl2  43483  setrec2  44700  aacllem  44804
  Copyright terms: Public domain W3C validator