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  928  nanbi  1491  rb-bijust  1751  sbnf2  2379  sb8mo  2688  cbvmowOLD  2690  raleqbii  3228  rmo5  3417  cbvrmowOLD  3429  cbvrmo  3433  ss2ab  4025  sbcssg  4446  ssextss  5333  relop  5708  dmcosseq  5831  cotrg  5958  cnvsym  5961  intasym  5962  intirr  5965  codir  5967  qfto  5968  cnvpo  6125  dff14a  7020  porpss  7447  funcnvuni  7631  poxp  7818  infcllem  8948  cp  9317  aceq2  9543  kmlem12  9585  kmlem15  9588  zfcndpow  10036  grothprim  10254  dfinfre  11618  infrenegsup  11620  xrinfmss2  12701  algcvgblem  15919  isprm2  16024  oduglb  17749  odulub  17751  isirred2  19454  isdomn2  20072  ntreq0  21685  ist0-3  21953  ist1-3  21957  ordthaus  21992  dfconn2  22027  iscusp2  22911  mdsymlem8  30196  mo5f  30262  iuninc  30323  suppss2f  30395  tosglblem  30667  esumpfinvalf  31392  bnj110  32187  bnj92  32191  bnj539  32220  bnj540  32221  axrepprim  32985  axacprim  32990  dffr5  33046  dfso2  33047  dfpo2  33048  elpotr  33083  bj-alcomexcom  34071  itg2addnclem2  35054  isdmn3  35457  sbcimi  35493  ssrel3  35661  inxpss3  35676  trcoss2  35829  moxfr  39549  isdomn3  40064  ifpim123g  40124  elmapintrab  40192  undmrnresiss  40220  cnvssco  40222  snhesn  40404  psshepw  40406  frege77  40558  frege93  40574  frege116  40597  frege118  40599  frege131  40612  frege133  40614  ntrneikb  40716  ismnuprim  40922  onfrALTlem5  41168  onfrALTlem5VD  41511  setis  45153
  Copyright terms: Public domain W3C validator