ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  biimpri Structured version   GIF version

Theorem biimpri 124
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 123 . 2 (ψφ)
32biimpi 113 1 (ψφ)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  sylbir  125  mpbir  134  sylibr  137  syl5bir  142  syl6ibr  151  bitri  173  sylanbr  269  sylan2br  272  simplbi2  367  pm3.43OLD  523  mtbi  582  pm3.44  622  orbi2i  666  pm2.31  672  dcor  831  rnlem  871  syl3an1br  1160  syl3an2br  1161  syl3an3br  1162  xorbin  1258  3impexpbicom  1306  equveli  1624  sbbii  1630  dveeq2or  1679  exmoeudc  1945  eueq2dc  2691  ralun  3102  undif3ss  3175  ssunieq  3587  a9evsep  3853  suctr  4108  tfi  4232  peano5  4248  opelxpi  4303  ndmima  4629  iotass  4811  dffo2  5035  dff1o2  5056  resdif  5073  f1o00  5086  ressnop0  5269  fsnunfv  5288  ovid  5540  ovidig  5541  f1stres  5709  f2ndres  5710  frec0g  5902  ltexnqq  6266  enq0sym  6287  prarloclem5  6354  nqprloc  6400  axcnre  6575  bj-sucexg  7145  bj-2inf  7160  peano5set  7162  findset  7167
  Copyright terms: Public domain W3C validator