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

Theorem imbi12i 339
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 335 . 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  928  nanbi  1603  rb-bijust  1823  nfbiiOLD  1985  sbnf2  2576  sb8mo  2642  cbvmo  2644  raleqbii  3128  rmo5  3301  cbvrmo  3309  ss2ab  3811  sbcssg  4229  trint  4920  ssextss  5071  relop  5428  dmcosseq  5542  cotrg  5665  issref  5667  cnvsym  5668  intasym  5669  intirr  5672  codir  5674  qfto  5675  cnvpo  5834  dff14a  6690  porpss  7106  funcnvuni  7284  poxp  7457  infcllem  8558  cp  8927  aceq2  9132  kmlem12  9175  kmlem15  9178  zfcndpow  9630  grothprim  9848  dfinfre  11196  infrenegsup  11198  xrinfmss2  12334  algcvgblem  15492  isprm2  15597  oduglb  17340  odulub  17342  isirred2  18901  isdomn2  19501  ntreq0  21083  ist0-3  21351  ist1-3  21355  ordthaus  21390  dfconn2  21424  iscusp2  22307  mdsymlem8  29578  mo5f  29633  iuninc  29686  suppss2f  29748  tosglblem  29978  esumpfinvalf  30447  bnj110  31235  bnj92  31239  bnj539  31268  bnj540  31269  axrepprim  31886  axacprim  31891  dffr5  31950  dfso2  31951  dfpo2  31952  elpotr  31991  gtinfOLD  32620  bj-alcomexcom  32976  itg2addnclem2  33775  isdmn3  34186  sbcimi  34225  ssrel3  34391  inxpss3  34408  trcoss2  34557  moxfr  37757  isdomn3  38284  ifpim123g  38347  elmapintrab  38384  undmrnresiss  38412  cnvssco  38414  snhesn  38582  psshepw  38584  frege77  38736  frege93  38752  frege116  38775  frege118  38777  frege131  38790  frege133  38792  ntrneikb  38894  conss34OLD  39148  onfrALTlem5  39259  onfrALTlem5VD  39620  setis  42954
  Copyright terms: Public domain W3C validator