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

Theorem imbi12i 341
Description: Join two logical equivalences to form equivalence of implications. (Contributed by NM, 1-Aug-1993.)
Hypotheses
Ref Expression
imbi12i.1 (𝜑𝜓)
imbi12i.2 (𝜒𝜃)
Assertion
Ref Expression
imbi12i ((𝜑𝜒) ↔ (𝜓𝜃))

Proof of Theorem imbi12i
StepHypRef Expression
1 imbi12i.1 . 2 (𝜑𝜓)
2 imbi12i.2 . 2 (𝜒𝜃)
3 imbi12 337 . 2 ((𝜑𝜓) → ((𝜒𝜃) → ((𝜑𝜒) ↔ (𝜓𝜃))))
41, 2, 3mp2 9 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:  orimdi  945  nanbi  1608  rb-bijust  1829  nfbiiOLD  1998  sbnf2  2600  sb8mo  2664  cbvmo  2666  raleqbii  3174  rmo5  3347  cbvrmo  3355  ss2ab  3861  sbcssg  4272  trint  4954  ssextss  5106  relop  5468  dmcosseq  5582  cotrg  5711  idrefOLD  5714  cnvsym  5715  intasym  5716  intirr  5719  codir  5721  qfto  5722  cnvpo  5881  dff14a  6745  porpss  7165  funcnvuni  7343  poxp  7517  infcllem  8626  cp  8995  aceq2  9219  kmlem12  9262  kmlem15  9265  zfcndpow  9717  grothprim  9935  dfinfre  11283  infrenegsup  11285  xrinfmss2  12353  algcvgblem  15503  isprm2  15607  oduglb  17338  odulub  17340  isirred2  18897  isdomn2  19502  ntreq0  21089  ist0-3  21357  ist1-3  21361  ordthaus  21396  dfconn2  21430  iscusp2  22313  mdsymlem8  29591  mo5f  29646  iuninc  29698  suppss2f  29760  tosglblem  29988  esumpfinvalf  30457  bnj110  31245  bnj92  31249  bnj539  31278  bnj540  31279  axrepprim  31895  axacprim  31900  dffr5  31959  dfso2  31960  dfpo2  31961  elpotr  32000  gtinfOLD  32629  bj-alcomexcom  32979  itg2addnclem2  33768  isdmn3  34178  sbcimi  34217  ssrel3  34378  inxpss3  34394  trcoss2  34541  moxfr  37751  isdomn3  38277  ifpim123g  38339  elmapintrab  38376  undmrnresiss  38404  cnvssco  38406  snhesn  38574  psshepw  38576  frege77  38728  frege93  38744  frege116  38767  frege118  38769  frege131  38782  frege133  38784  ntrneikb  38886  onfrALTlem5  39249  onfrALTlem5VD  39609  setis  43006
  Copyright terms: Public domain W3C validator