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

Theorem imbi12i 352
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 348 . 2 ((𝜑𝜓) → ((𝜒𝜃) → ((𝜑𝜒) ↔ (𝜓𝜃))))
41, 2, 3mp2 9 1 ((𝜑𝜒) ↔ (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207
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 208
This theorem is referenced by:  orimdi  924  nanbi  1484  rb-bijust  1741  sbnf2  2368  sb8mo  2680  cbvmow  2681  raleqbii  3231  rmo5  3432  cbvrmow  3442  cbvrmo  3446  ss2ab  4036  sbcssg  4459  ssextss  5337  relop  5714  dmcosseq  5837  cotrg  5964  cnvsym  5967  intasym  5968  intirr  5971  codir  5973  qfto  5974  cnvpo  6131  dff14a  7019  porpss  7442  funcnvuni  7625  poxp  7811  infcllem  8939  cp  9308  aceq2  9533  kmlem12  9575  kmlem15  9578  zfcndpow  10026  grothprim  10244  dfinfre  11610  infrenegsup  11612  xrinfmss2  12692  algcvgblem  15909  isprm2  16014  oduglb  17737  odulub  17739  isirred2  19380  isdomn2  20000  ntreq0  21613  ist0-3  21881  ist1-3  21885  ordthaus  21920  dfconn2  21955  iscusp2  22838  mdsymlem8  30114  mo5f  30180  iuninc  30240  suppss2f  30312  tosglblem  30583  esumpfinvalf  31234  bnj110  32029  bnj92  32033  bnj539  32062  bnj540  32063  axrepprim  32825  axacprim  32830  dffr5  32886  dfso2  32887  dfpo2  32888  elpotr  32923  bj-alcomexcom  33911  itg2addnclem2  34825  isdmn3  35233  sbcimi  35269  ssrel3  35437  inxpss3  35452  trcoss2  35604  moxfr  39167  isdomn3  39682  ifpim123g  39744  elmapintrab  39814  undmrnresiss  39842  cnvssco  39844  snhesn  40010  psshepw  40012  frege77  40164  frege93  40180  frege116  40203  frege118  40205  frege131  40218  frege133  40220  ntrneikb  40322  ismnuprim  40507  onfrALTlem5  40753  onfrALTlem5VD  41096  setis  44728
  Copyright terms: Public domain W3C validator