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  1820  spsbbi  2079  cbv2w  2342  cbv2  2408  cbv2h  2411  dfmoeu  2536  2eu6  2658  ax9ALT  2732  ralbi  3093  rexbi  3094  ceqsalt  3476  spcgft  3508  vtoclgft  3511  elabgtOLD  3629  elabgtOLDOLD  3630  reu6  3686  reu3  3687  sbciegftOLD  3780  axpr  5374  axprlem4OLD  5376  fv3  6860  elirrv  9514  expeq0  14027  t1t0  23304  kqfvima  23686  ufileu  23875  axsepg2ALT  35258  r1omhfb  35287  r1omhfbregs  35312  cvmlift2lem1  35515  btwndiff  36240  nn0prpw  36536  bj-bisimpl  36774  bj-bisimpr  36775  bj-animbi  36780  bj-dfbi6  36797  bj-bi3ant  36811  bj-cbv2hv  37042  bj-moeub  37094  bj-ceqsalt0  37129  bj-ceqsalt1  37130  eqab2  38498  sticksstones3  42515  eu6w  43031  or3or  44376  bi33imp12  44844  bi23imp1  44848  bi123imp0  44849  eqsbc2VD  45192  imbi12VD  45225  2uasbanhVD  45263  ssclaxsep  45335  nimnbi  45519  thincciso  49809