Theorem biimp 215

Description: Property of the biconditional connective. (Contributed by NM, 11-May-1999.)

Assertion

Ref	Expression
biimp	⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓))

Proof of Theorem biimp

Step	Hyp	Ref	Expression
1		df-bi 207	. . 3 ⊢ ¬ (((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) → ¬ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓)))
2		simplim 167	. . 3 ⊢ (¬ (((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) → ¬ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓))) → ((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))))
3	1, 2	ax-mp 5	. 2 ⊢ ((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)))
4		simplim 167	. 2 ⊢ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜑 → 𝜓))
5	3, 4	syl 17	1 ⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  biimpi  216  bicom1  221  biimpd  229  ibd  269  pm5.74  270  pm5.501  366  bija  380  albi  1818  spsbbi  2074  cbv2w  2335  cbv2  2402  cbv2h  2405  dfmoeu  2530  2eu6  2651  ax9ALT  2725  ralbi  3086  rexbi  3087  ceqsalt  3484  spcgft  3518  vtoclgft  3521  elabgtOLD  3642  elabgtOLDOLD  3643  reu6  3700  reu3  3701  sbciegftOLD  3794  axpr  5385  axprlem4OLD  5387  fv3  6879  expeq0  14064  t1t0  23242  kqfvima  23624  ufileu  23813  axsepg2ALT  35080  cvmlift2lem1  35296  btwndiff  36022  nn0prpw  36318  bj-animbi  36554  bj-dfbi6  36570  bj-bi3ant  36584  bj-cbv2hv  36792  bj-moeub  36844  bj-ceqsalt0  36879  bj-ceqsalt1  36880  eqab2  38244  sticksstones3  42143  eu6w  42671  or3or  44019  bi33imp12  44488  bi23imp1  44492  bi123imp0  44493  eqsbc2VD  44836  imbi12VD  44869  2uasbanhVD  44907  ssclaxsep  44979  nimnbi  45164  thincciso  49446