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

Theorem imbi12i 340
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 336 . 2 ((𝜑𝜓) → ((𝜒𝜃) → ((𝜑𝜒) ↔ (𝜓𝜃))))
41, 2, 3mp2 9 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:  orimdi  891  nanbi  1451  rb-bijust  1671  nfbiiOLD  1833  sbnf2  2438  sb8mo  2503  cbvmo  2505  raleqbii  2986  rmo5  3155  cbvrmo  3162  ss2ab  3655  sbcssg  4063  trint  4738  ssextss  4893  relop  5242  dmcosseq  5357  cotrg  5476  issref  5478  cnvsym  5479  intasym  5480  intirr  5483  codir  5485  qfto  5486  cnvpo  5642  dff14a  6492  porpss  6906  funcnvuni  7081  poxp  7249  infcllem  8353  cp  8714  aceq2  8902  kmlem12  8943  kmlem15  8946  zfcndpow  9398  grothprim  9616  dfinfre  10964  infrenegsup  10966  xrinfmss2  12100  algcvgblem  15233  isprm2  15338  oduglb  17079  odulub  17081  isirred2  18641  isdomn2  19239  ntreq0  20821  ist0-3  21089  ist1-3  21093  ordthaus  21128  dfconn2  21162  iscusp2  22046  frgr2wwlkeqm  27088  mdsymlem8  29157  mo5f  29213  iuninc  29265  suppss2f  29322  tosglblem  29496  esumpfinvalf  29961  bnj110  30689  bnj92  30693  bnj539  30722  bnj540  30723  axrepprim  31340  axacprim  31345  dffr5  31404  dfso2  31405  dfpo2  31406  elpotr  31440  gtinfOLD  32009  bj-alcomexcom  32365  itg2addnclem2  33133  isdmn3  33544  sbcimi  33583  moxfr  36774  isdomn3  37302  ifpim123g  37365  elmapintrab  37402  undmrnresiss  37430  cnvssco  37432  snhesn  37601  psshepw  37603  frege77  37755  frege93  37771  frege116  37794  frege118  37796  frege131  37809  frege133  37811  ntrneikb  37913  conss34OLD  38167  onfrALTlem5  38278  onfrALTlem5VD  38643
  Copyright terms: Public domain W3C validator