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

Theorem imbi1i 340
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 338 . 2 ((𝜑𝜓) → ((𝜑𝜒) ↔ (𝜓𝜒)))
31, 2ax-mp 5 1 ((𝜑𝜒) ↔ (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197
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 198
This theorem is referenced by:  ancomst  452  imor  871  ifpn  1088  eximal  1862  19.43  1972  19.37v  2090  19.37  2269  dfsb3  2535  sbrim  2557  sbor  2559  mo4f  2690  2mos  2727  neor  3080  r3al  3139  r19.23t  3220  r19.23v  3222  r19.43  3292  ceqsralt  3434  ralab  3574  ralrab  3575  euind  3602  reu2  3603  rmo4  3608  reuind  3620  2reu5lem3  3624  rmo3  3734  dfdif3  3930  raldifb  3960  unss  3997  ralunb  4004  inssdif0  4159  dfnf5  4164  ssundif  4259  dfif2  4292  pwss  4379  ralsnsg  4420  disjsn  4449  snssg  4516  raldifsni  4527  raldifsnb  4528  unissb  4674  intun  4712  intpr  4713  dfiin2g  4756  disjor  4837  dftr2  4959  axrep1  4978  axpweq  5047  zfpow  5049  axpow2  5050  reusv2lem4  5083  reusv2  5085  raliunxp  5477  idrefALT  5733  asymref2  5738  dffun2  6121  dffun4  6123  dffun5  6124  dffun7  6138  fununi  6185  fvn0ssdmfun  6582  dff13  6746  dff14b  6762  zfun  7190  uniex2  7192  dfom2  7307  fimaxg  8456  fiint  8486  dfsup2  8599  fiming  8653  oemapso  8836  scottexs  9007  scott0s  9008  iscard2  9095  acnnum  9168  dfac9  9253  dfacacn  9258  kmlem4  9270  kmlem12  9278  axpowndlem3  9716  zfcndun  9732  zfcndpow  9733  zfcndac  9736  axgroth5  9941  grothpw  9943  axgroth6  9945  addsrmo  10189  mulsrmo  10190  infm3  11277  raluz2  11975  nnwos  11994  ralrp  12086  cotr2g  13960  lo1resb  14538  rlimresb  14539  o1resb  14540  modfsummod  14768  isprm4  15635  acsfn1  16546  acsfn2  16548  lublecllem  17213  isirred2  18923  isdomn2  19528  iunocv  20256  ist1-2  21386  isnrm2  21397  dfconn2  21457  alexsubALTlem3  22087  ismbl  23530  dyadmbllem  23603  ellimc3  23880  dchrelbas2  25199  dchrelbas3  25200  isch2  28431  choc0  28536  h1dei  28760  mdsl2i  29532  rmo3f  29684  rmo4fOLD  29685  rmo4f  29686  disjorf  29740  bnj1101  31200  bnj1109  31202  bnj1533  31267  bnj580  31328  bnj864  31337  bnj865  31338  bnj978  31364  bnj1049  31387  bnj1090  31392  bnj1145  31406  axextprim  31922  axunprim  31924  axpowprim  31925  untuni  31930  3orit  31940  biimpexp  31941  elintfv  32006  dfon2lem8  32037  soseq  32097  dfom5b  32362  bj-axrep1  33121  bj-zfpow  33128  bj-raldifsn  33384  rdgeqoa  33553  wl-equsalcom  33661  poimirlem25  33766  poimirlem30  33771  tsim1  34266  inxpss  34417  idinxpss  34418  idinxpssinxp  34422  ineleq  34451  cocossss  34523  cosscnvssid3  34558  trcoss2  34566  cvlsupr3  35143  pmapglbx  35568  isltrn2N  35919  cdlemefrs29bpre0  36195  fphpd  37900  dford4  38115  fnwe2lem2  38140  isdomn3  38301  ifpidg  38354  ifpid1g  38357  ifpor123g  38371  undmrnresiss  38428  elintima  38463  df3or2  38578  dfhe3  38587  dffrege76  38751  dffrege115  38790  frege131  38806  ntrneikb  38910  ntrneixb  38911  pm14.12  39139  dfvd2an  39314  dfvd3  39323  dfvd3an  39326  uun2221  39555  uun2221p1  39556  uun2221p2  39557  disjinfi  39887  supxrleubrnmptf  40177  fsummulc1f  40300  fsumiunss  40305  fnlimfvre2  40407  limsupreuz  40467  limsupvaluz2  40468  dvmptmulf  40650  dvnmul  40656  dvmptfprodlem  40657  dvnprodlem2  40660  sge0ltfirpmpt2  41140  hoidmv1le  41308  hoidmvle  41314  vonioolem2  41395  smflimlem3  41481  setrec2  43028  aacllem  43136
  Copyright terms: Public domain W3C validator