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

Theorem biimpri 197
Description: Infer a converse implication from a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 16-Sep-2013.)
Hypothesis
Ref Expression
biimpri.1 (φψ)
Assertion
Ref Expression
biimpri (ψφ)

Proof of Theorem biimpri
StepHypRef Expression
1 biimpri.1 . . 3 (φψ)
21bicomi 193 . 2 (ψφ)
32biimpi 186 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:  mpbir  200  sylibr  203  sylbir  204  syl5bir  209  syl6ibr  218  bitri  240  mtbi  289  pm2.54  363  sylanbr  459  sylan2br  462  pm3.11  485  orbi2i  505  pm2.31  511  simplbi2  608  dfbi  610  pm2.85  826  rnlem  931  syl3an1br  1221  syl3an2br  1222  syl3an3br  1223  3impexpbicom  1367  nic-axALT  1439  sbbii  1653  hbn1fw  1705  equveli  1988  exmoeu  2246  eueq2  3010  ralun  3445  ssunieq  3924  cnvkexg  4286  p6exg  4290  ssetkex  4294  sikexg  4296  ins2kexg  4305  ins3kexg  4306  peano5  4409  ltfinirr  4457  spfininduct  4540  vfinspnn  4541  opbrop  4841  ndmima  5025  dminss  5041  dffo2  5273  dff1o2  5291  resdif  5306  f1o00  5317  ressnop0  5436  ovg  5601  clos1induct  5880  ssetpov  5944  nenpw1pwlem2  6085  sbthlem1  6203
  Copyright terms: Public domain W3C validator