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

Theorem imbi1i 339
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 337 . 2 ((𝜑𝜓) → ((𝜑𝜒) ↔ (𝜓𝜒)))
31, 2ax-mp 5 1 ((𝜑𝜒) ↔ (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
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 197
This theorem is referenced by:  imor  428  ancomst  468  ifpn  1021  eximal  1705  19.43  1808  19.37v  1908  19.37  2098  dfsb3  2372  sbrim  2394  sbor  2396  mo4f  2514  2mos  2550  neor  2882  r3al  2937  r19.23t  3017  r19.23v  3019  r19.43  3088  ceqsralt  3224  ralab  3361  ralrab  3362  euind  3387  reu2  3388  rmo4  3393  reuind  3405  2reu5lem3  3409  rmo3  3521  raldifb  3742  unss  3779  ralunb  3786  inssdif0  3938  dfnf5  3943  ssundif  4043  dfif2  4079  pwss  4166  ralsnsg  4207  disjsn  4237  snss  4307  raldifsni  4315  raldifsnb  4316  unissb  4460  intun  4500  intpr  4501  dfiin2g  4544  disjor  4625  dftr2  4745  axrep1  4763  axpweq  4833  zfpow  4835  axpow2  4836  reusv2lem4  4863  reusv2  4865  raliunxp  5250  asymref2  5501  dffun2  5886  dffun4  5888  dffun5  5889  dffun7  5903  fununi  5952  fvn0ssdmfun  6336  dff13  6497  dff14b  6513  zfun  6935  uniex2  6937  dfom2  7052  fimaxg  8192  fiint  8222  dfsup2  8335  fiming  8389  oemapso  8564  scottexs  8735  scott0s  8736  iscard2  8787  acnnum  8860  dfac9  8943  dfacacn  8948  kmlem4  8960  kmlem12  8968  axpowndlem3  9406  zfcndun  9422  zfcndpow  9423  zfcndac  9426  axgroth5  9631  grothpw  9633  axgroth6  9635  addsrmo  9879  mulsrmo  9880  infm3  10967  raluz2  11722  nnwos  11740  ralrp  11837  cotr2g  13696  lo1resb  14276  rlimresb  14277  o1resb  14278  modfsummod  14507  isprm4  15378  acsfn1  16303  acsfn2  16305  lublecllem  16969  isirred2  18682  isdomn2  19280  iunocv  20006  ist1-2  21132  isnrm2  21143  dfconn2  21203  alexsubALTlem3  21834  ismbl  23275  dyadmbllem  23348  ellimc3  23624  dchrelbas2  24943  dchrelbas3  24944  isch2  28050  choc0  28155  h1dei  28379  mdsl2i  29151  rmo3f  29307  rmo4fOLD  29308  rmo4f  29309  disjorf  29364  bnj538OLD  30784  bnj1101  30829  bnj1109  30831  bnj1533  30896  bnj580  30957  bnj864  30966  bnj865  30967  bnj978  30993  bnj1049  31016  bnj1090  31021  bnj1145  31035  axextprim  31552  axunprim  31554  axpowprim  31555  untuni  31560  3orit  31571  biimpexp  31572  elintfv  31638  dfon2lem8  31669  soseq  31725  dfom5b  31994  bj-axrep1  32763  bj-zfpow  32770  bj-raldifsn  33029  rdgeqoa  33189  wl-equsalcom  33299  poimirlem25  33405  poimirlem30  33410  tsim1  33908  cvlsupr3  34450  pmapglbx  34874  isltrn2N  35225  cdlemefrs29bpre0  35503  fphpd  37199  dford4  37415  fnwe2lem2  37440  isdomn3  37601  ifpidg  37655  ifpid1g  37658  ifpor123g  37672  undmrnresiss  37729  elintima  37764  df3or2  37879  dfhe3  37889  dffrege76  38053  dffrege115  38092  frege131  38108  ntrneikb  38212  ntrneixb  38213  pm14.12  38442  dfvd2an  38618  dfvd3  38627  dfvd3an  38630  uun2221  38860  uun2221p1  38861  uun2221p2  38862  disjinfi  39196  supxrleubrnmptf  39493  fsummulc1f  39602  fsumiunss  39607  fnlimfvre2  39709  limsupreuz  39769  limsupvaluz2  39770  dvmptmulf  39915  dvnmul  39921  dvmptfprodlem  39922  dvnprodlem2  39925  sge0ltfirpmpt2  40406  hoidmv1le  40571  hoidmvle  40577  vonioolem2  40658  smflimlem3  40744  setrec2  42207  aacllem  42312
  Copyright terms: Public domain W3C validator