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  2073  cbv2w  2338  cbv2  2407  cbv2h  2410  dfmoeu  2535  2eu6  2656  ax9ALT  2730  ralbi  3092  rexbi  3093  ceqsalt  3494  spcgft  3528  vtoclgft  3531  elabgt  3651  elabgtOLD  3652  reu6  3709  reu3  3710  sbciegftOLD  3803  axpr  5397  axprlem4OLD  5399  fv3  6894  expeq0  14110  t1t0  23286  kqfvima  23668  ufileu  23857  axsepg2ALT  35114  cvmlift2lem1  35324  btwndiff  36045  nn0prpw  36341  bj-animbi  36577  bj-dfbi6  36593  bj-bi3ant  36607  bj-cbv2hv  36815  bj-moeub  36867  bj-ceqsalt0  36902  bj-ceqsalt1  36903  sticksstones3  42161  eu6w  42699  or3or  44047  bi33imp12  44516  bi23imp1  44520  bi123imp0  44521  eqsbc2VD  44864  imbi12VD  44897  2uasbanhVD  44935  ssclaxsep  45007  nimnbi  45187  thincciso  49339