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  1816  spsbbi  2073  cbv2w  2343  cbv2  2411  cbv2h  2414  dfmoeu  2539  2eu6  2660  ax9ALT  2735  ralbi  3109  rexbi  3110  ceqsalt  3523  spcgft  3561  vtoclgft  3564  elabgt  3685  elabgtOLD  3686  reu6  3748  reu3  3749  sbciegftOLD  3843  axprlem4  5444  fv3  6938  expeq0  14143  t1t0  23377  kqfvima  23759  ufileu  23948  axsepg2ALT  35059  cvmlift2lem1  35270  btwndiff  35991  nn0prpw  36289  bj-animbi  36525  bj-dfbi6  36541  bj-bi3ant  36555  bj-cbv2hv  36763  bj-moeub  36815  bj-ceqsalt0  36850  bj-ceqsalt1  36851  sticksstones3  42105  eu6w  42631  or3or  43985  bi33imp12  44461  bi23imp1  44466  bi123imp0  44467  eqsbc2VD  44811  imbi12VD  44844  2uasbanhVD  44882  nimnbi  45069  thincciso  48716