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

Theorem imbi1i 338
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 336 . 2 ((𝜑𝜓) → ((𝜑𝜒) ↔ (𝜓𝜒)))
31, 2ax-mp 5 1 ((𝜑𝜒) ↔ (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195
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 196
This theorem is referenced by:  imor  427  ancomst  467  ifpn  1016  eximal  1698  19.43  1799  19.37v  1897  19.37  2087  dfsb3  2362  sbrim  2384  sbor  2386  mo4f  2504  2mos  2540  neor  2873  r3al  2924  r19.23t  3003  r19.23v  3005  r19.43  3074  ceqsralt  3202  ralab  3334  ralrab  3335  euind  3360  reu2  3361  rmo4  3366  reuind  3378  2reu5lem3  3382  rmo3  3494  raldifb  3712  unss  3749  ralunb  3756  inssdif0  3901  dfnf5  3906  ssundif  4004  dfif2  4038  pwss  4123  ralsnsg  4163  disjsn  4192  snss  4259  raldifsni  4265  raldifsnb  4266  unissb  4405  intun  4444  intpr  4445  dfiin2g  4489  disjor  4567  dftr2  4682  axrep1  4700  axpweq  4768  zfpow  4770  axpow2  4771  reusv2lem4  4798  reusv2  4800  raliunxp  5183  asymref2  5432  dffun2  5814  dffun4  5816  dffun5  5817  dffun7  5830  fununi  5878  fvn0ssdmfun  6258  dff13  6416  dff14b  6428  zfun  6848  uniex2  6850  dfom2  6959  fimaxg  8092  fiint  8122  dfsup2  8233  fiming  8287  oemapso  8462  scottexs  8633  scott0s  8634  iscard2  8685  acnnum  8758  dfac9  8841  dfacacn  8846  kmlem4  8858  kmlem12  8866  axpowndlem3  9300  zfcndun  9316  zfcndpow  9317  zfcndac  9320  axgroth5  9525  grothpw  9527  axgroth6  9529  addsrmo  9773  mulsrmo  9774  infm3  10861  raluz2  11613  nnwos  11631  ralrp  11728  cotr2g  13563  lo1resb  14143  rlimresb  14144  o1resb  14145  modfsummod  14367  isprm4  15235  acsfn1  16145  acsfn2  16147  lublecllem  16811  isirred2  18524  isdomn2  19120  iunocv  19844  ist1-2  20961  isnrm2  20972  dfcon2  21032  alexsubALTlem3  21663  ismbl  23101  dyadmbllem  23173  ellimc3  23449  dchrelbas2  24762  dchrelbas3  24763  isch2  27464  choc0  27569  h1dei  27793  mdsl2i  28565  rmo3f  28719  rmo4fOLD  28720  rmo4f  28721  disjorf  28774  bnj538OLD  30064  bnj1101  30109  bnj1109  30111  bnj1533  30176  bnj580  30237  bnj864  30246  bnj865  30247  bnj978  30273  bnj1049  30296  bnj1090  30301  bnj1145  30315  axextprim  30832  axunprim  30834  axpowprim  30835  untuni  30840  3orit  30851  biimpexp  30852  dfon2lem8  30939  soseq  30995  dfom5b  31189  bj-axrep1  31976  bj-zfpow  31983  rdgeqoa  32394  wl-equsalcom  32507  poimirlem25  32604  poimirlem30  32609  tsim1  33107  cvlsupr3  33649  pmapglbx  34073  isltrn2N  34424  cdlemefrs29bpre0  34702  fphpd  36398  dford4  36614  fnwe2lem2  36639  isdomn3  36801  ifpidg  36855  ifpid1g  36858  ifpor123g  36872  undmrnresiss  36929  elintima  36964  df3or2  37079  dfhe3  37089  dffrege76  37253  dffrege115  37292  frege131  37308  ntrneikb  37412  ntrneixb  37413  pm14.12  37644  dfvd2an  37819  dfvd3  37828  dfvd3an  37831  uun2221  38061  uun2221p1  38062  uun2221p2  38063  disjinfi  38375  fsummulc1f  38635  fsumiunss  38642  fnlimfvre2  38744  dvmptmulf  38827  dvnmul  38833  dvmptfprodlem  38834  dvnprodlem2  38837  sge0ltfirpmpt2  39319  hoidmv1le  39484  hoidmvle  39490  vonioolem2  39572  smflimlem3  39659  setrec2  42241  aacllem  42356
  Copyright terms: Public domain W3C validator