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

Theorem imbi1i 337
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 335 . 2 ((𝜑𝜓) → ((𝜑𝜒) ↔ (𝜓𝜒)))
31, 2ax-mp 5 1 ((𝜑𝜒) ↔ (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194
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 195
This theorem is referenced by:  imor  426  ancomst  466  ifpn  1015  eximal  1697  19.43  1798  19.37v  1896  19.37  2085  dfsb3  2358  sbrim  2380  sbor  2382  mo4f  2500  2mos  2536  neor  2869  r3al  2920  r19.23t  2999  r19.23v  3001  r19.43  3070  ceqsralt  3198  ralab  3330  ralrab  3331  euind  3356  reu2  3357  rmo4  3362  reuind  3374  2reu5lem3  3378  rmo3  3490  raldifb  3708  unss  3745  ralunb  3752  inssdif0  3897  dfnf5  3902  ssundif  4000  dfif2  4034  pwss  4119  ralsnsg  4159  disjsn  4188  snss  4255  raldifsni  4261  raldifsnb  4262  unissb  4396  intun  4435  intpr  4436  dfiin2g  4480  disjor  4558  dftr2  4673  axrep1  4691  axpweq  4760  zfpow  4762  axpow2  4763  reusv2lem4  4790  reusv2  4792  raliunxp  5168  asymref2  5416  dffun2  5797  dffun4  5799  dffun5  5800  dffun7  5813  fununi  5861  fvn0ssdmfun  6240  dff13  6391  dff14b  6403  zfun  6822  uniex2  6824  dfom2  6933  fimaxg  8066  fiint  8096  dfsup2  8207  fiming  8261  oemapso  8436  scottexs  8607  scott0s  8608  iscard2  8659  acnnum  8732  dfac9  8815  dfacacn  8820  kmlem4  8832  kmlem12  8840  axpowndlem3  9274  zfcndun  9290  zfcndpow  9291  zfcndac  9294  axgroth5  9499  grothpw  9501  axgroth6  9503  addsrmo  9747  mulsrmo  9748  infm3  10828  raluz2  11566  nnwos  11584  ralrp  11681  cotr2g  13506  lo1resb  14086  rlimresb  14087  o1resb  14088  modfsummod  14310  isprm4  15178  acsfn1  16088  acsfn2  16090  lublecllem  16754  isirred2  18467  isdomn2  19063  iunocv  19783  ist1-2  20900  isnrm2  20911  dfcon2  20971  alexsubALTlem3  21602  ismbl  23015  dyadmbllem  23087  ellimc3  23363  dchrelbas2  24676  dchrelbas3  24677  isch2  27267  choc0  27372  h1dei  27596  mdsl2i  28368  rmo3f  28522  rmo4fOLD  28523  rmo4f  28524  disjorf  28577  bnj538OLD  29867  bnj1101  29912  bnj1109  29914  bnj1533  29979  bnj580  30040  bnj864  30049  bnj865  30050  bnj978  30076  bnj1049  30099  bnj1090  30104  bnj1145  30118  axextprim  30635  axunprim  30637  axpowprim  30638  untuni  30643  3orit  30654  biimpexp  30655  dfon2lem8  30742  soseq  30798  dfom5b  30992  bj-axrep1  31786  bj-zfpow  31793  rdgeqoa  32194  wl-equsalcom  32307  poimirlem25  32404  poimirlem30  32409  tsim1  32907  cvlsupr3  33449  pmapglbx  33873  isltrn2N  34224  cdlemefrs29bpre0  34502  fphpd  36198  dford4  36414  fnwe2lem2  36439  isdomn3  36601  ifpidg  36655  ifpid1g  36658  ifpor123g  36672  undmrnresiss  36729  elintima  36764  df3or2  36879  dfhe3  36889  dffrege76  37053  dffrege115  37092  frege131  37108  ntrneikb  37212  ntrneixb  37213  pm14.12  37444  dfvd2an  37619  dfvd3  37628  dfvd3an  37631  uun2221  37861  uun2221p1  37862  uun2221p2  37863  disjinfi  38175  fsummulc1f  38436  fsumiunss  38443  fnlimfvre2  38545  dvmptmulf  38628  dvnmul  38634  dvmptfprodlem  38635  dvnprodlem2  38638  sge0ltfirpmpt2  39120  hoidmv1le  39285  hoidmvle  39291  vonioolem2  39373  smflimlem3  39460  aacllem  42316
  Copyright terms: Public domain W3C validator