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  1819  spsbbi  2078  cbv2w  2341  cbv2  2407  cbv2h  2410  dfmoeu  2535  2eu6  2657  ax9ALT  2731  ralbi  3091  rexbi  3092  ceqsalt  3474  spcgft  3506  vtoclgft  3509  elabgtOLD  3627  elabgtOLDOLD  3628  reu6  3684  reu3  3685  sbciegftOLD  3778  axpr  5372  axprlem4OLD  5374  fv3  6852  elirrv  9502  expeq0  14015  t1t0  23292  kqfvima  23674  ufileu  23863  axsepg2ALT  35239  r1omhfb  35268  r1omhfbregs  35293  cvmlift2lem1  35496  btwndiff  36221  nn0prpw  36517  bj-animbi  36759  bj-dfbi6  36775  bj-bi3ant  36789  bj-cbv2hv  36998  bj-moeub  37050  bj-ceqsalt0  37085  bj-ceqsalt1  37086  bj-axnul  37276  eqab2  38446  sticksstones3  42402  eu6w  42919  or3or  44264  bi33imp12  44732  bi23imp1  44736  bi123imp0  44737  eqsbc2VD  45080  imbi12VD  45113  2uasbanhVD  45151  ssclaxsep  45223  nimnbi  45407  thincciso  49698