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  1815  spsbbi  2071  cbv2w  2338  cbv2  2406  cbv2h  2409  dfmoeu  2534  2eu6  2655  ax9ALT  2730  ralbi  3101  rexbi  3102  ceqsalt  3513  spcgft  3549  vtoclgft  3552  elabgt  3672  elabgtOLD  3673  reu6  3735  reu3  3736  sbciegftOLD  3830  axpr  5433  axprlem4OLD  5435  fv3  6925  expeq0  14130  t1t0  23372  kqfvima  23754  ufileu  23943  axsepg2ALT  35076  cvmlift2lem1  35287  btwndiff  36009  nn0prpw  36306  bj-animbi  36542  bj-dfbi6  36558  bj-bi3ant  36572  bj-cbv2hv  36780  bj-moeub  36832  bj-ceqsalt0  36867  bj-ceqsalt1  36868  sticksstones3  42130  eu6w  42663  or3or  44013  bi33imp12  44488  bi23imp1  44493  bi123imp0  44494  eqsbc2VD  44838  imbi12VD  44871  2uasbanhVD  44909  ssclaxsep  44947  nimnbi  45106  thincciso  48849