NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  impbid GIF version

Theorem impbid 183
Description: Deduce an equivalence from two implications. (Contributed by NM, 5-Aug-1993.) (Revised by Wolf Lammen, 3-Nov-2012.)
Hypotheses
Ref Expression
impbid.1 (φ → (ψχ))
impbid.2 (φ → (χψ))
Assertion
Ref Expression
impbid (φ → (ψχ))

Proof of Theorem impbid
StepHypRef Expression
1 impbid.1 . . 3 (φ → (ψχ))
2 impbid.2 . . 3 (φ → (χψ))
31, 2impbid21d 182 . 2 (φ → (φ → (ψχ)))
43pm2.43i 43 1 (φ → (ψχ))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 176
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 177
This theorem is referenced by:  bicom1  190  impbid1  194  impcon4bid  196  pm5.74  235  imbi1d  308  pm5.501  330  2falsed  340  impbida  805  dedlem0b  919  dedlema  920  dedlemb  921  albi  1564  exbi  1581  equequ1  1684  equequ1OLD  1685  elequ1  1713  elequ2  1715  19.21t  1795  19.23t  1800  19.23tOLD  1819  19.21tOLD  1863  sbequ12  1919  dral1  1965  cbv2h  1980  ax11b  1995  sbft  2025  sbied  2036  sbequ  2060  sb56  2098  sbal1  2126  exsb  2130  dral1-o  2154  eupickb  2269  eupickbi  2270  2eu2  2285  ceqsalt  2881  ceqex  2969  mob2  3016  reu6  3025  sbciegft  3076  eqsbc3r  3103  csbiebt  3172  sseq1  3292  reupick  3539  reupick2  3541  uneqdifeq  3638  iotaval  4350  lenltfin  4469  ncfineleq  4477  tfinltfin  4501  copsexg  4607  iss  5000  funssres  5144  tz6.12c  5347  fvimacnv  5403  elpreima  5407  fsn  5432  fconst2g  5452  fconst5  5455  f1ocnvfvb  5479  f1oiso2  5500  oprabid  5550  erth  5968  enprmaplem5  6080  ncdisjun  6136  ce0addcnnul  6179  ce0nnulb  6182  ceclb  6183  ltlenlec  6207  dflec2  6210  tlecg  6230  muc0or  6252  lecadd2  6266  ncslesuc  6267  nchoicelem8  6296
  Copyright terms: Public domain W3C validator