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

Theorem imbi12i 354
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 350 . 2 ((𝜑𝜓) → ((𝜒𝜃) → ((𝜑𝜒) ↔ (𝜓𝜃))))
41, 2, 3mp2 9 1 ((𝜑𝜒) ↔ (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209
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 210
This theorem is referenced by:  orimdi  931  nanbi  1496  rb-bijust  1757  sbnf2  2359  sb8mo  2602  cbvmowOLD  2605  raleqbii  3161  rmo5  3356  cbvrmowOLD  3368  cbvrmo  3372  ss2ab  3990  sbcssg  4452  ssextss  5355  relop  5737  dmcosseq  5860  cotrg  5994  cnvsym  5997  intasym  5998  intirr  6001  codir  6003  qfto  6004  cnvpo  6168  dfpo2  6177  dff14a  7104  porpss  7537  funcnvuni  7731  poxp  7919  infcllem  9133  cp  9537  aceq2  9763  kmlem12  9805  kmlem15  9808  zfcndpow  10260  grothprim  10478  dfinfre  11843  infrenegsup  11845  xrinfmss2  12931  algcvgblem  16167  isprm2  16272  odulub  17946  oduglb  17948  isirred2  19752  isdomn2  20370  ntreq0  22006  ist0-3  22274  ist1-3  22278  ordthaus  22313  dfconn2  22348  iscusp2  23231  mdsymlem8  30523  mo5f  30588  iuninc  30651  suppss2f  30725  tosglblem  31003  prmidl0  31372  esumpfinvalf  31788  bnj110  32582  bnj92  32586  bnj539  32615  bnj540  32616  axrepprim  33387  axacprim  33392  dffr5  33471  dfso2  33472  elpotr  33507  ttrclss  33550  bj-alcomexcom  34633  itg2addnclem2  35603  isdmn3  36006  sbcimi  36042  ssrel3  36208  inxpss3  36223  trcoss2  36376  moxfr  40265  isdomn3  40780  ifpim123g  40840  elmapintrab  40908  undmrnresiss  40936  cnvssco  40938  snhesn  41119  psshepw  41121  frege77  41273  frege93  41289  frege116  41312  frege118  41314  frege131  41327  frege133  41329  ntrneikb  41429  ismnuprim  41633  onfrALTlem5  41883  onfrALTlem5VD  42226  setis  46120
  Copyright terms: Public domain W3C validator