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

Theorem impbid2 195
 Description: Infer an equivalence from two implications. (Contributed by NM, 6-Mar-2007.) (Proof shortened by Wolf Lammen, 27-Sep-2013.)
Hypotheses
Ref Expression
impbid2.1 (ψχ)
impbid2.2 (φ → (χψ))
Assertion
Ref Expression
impbid2 (φ → (ψχ))

Proof of Theorem impbid2
StepHypRef Expression
1 impbid2.2 . . 3 (φ → (χψ))
2 impbid2.1 . . 3 (ψχ)
31, 2impbid1 194 . 2 (φ → (χψ))
43bicomd 192 1 (φ → (ψχ))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 176 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8 This theorem depends on definitions:  df-bi 177 This theorem is referenced by:  biimt  325  biorf  394  biorfi  396  pm4.72  846  biort  866  bimsc1  904  euan  2261  cgsexg  2890  cgsex2g  2891  cgsex4g  2892  elab3gf  2990  abidnf  3005  elsnc2g  3761  difsn  3845  eqsn  3867  dfnfc2  3909  intmin4  3955  dfiin2g  4000  eqpw1uni  4330  eqfnfv  5392  ffvresb  5431  fnoprabg  5585  ncssfin  6151  ce0lenc1  6239
 Copyright terms: Public domain W3C validator