Theorem mtbird 715

Description: A deduction from a biconditional, similar to modus tollens.

Hypotheses

Ref	Expression
mtbird.min	|- (ph -> -. ch)
mtbird.maj	|- (ph -> (ps <-> ch))

Assertion

Ref	Expression
mtbird	|- (ph -> -. ps)

Proof of Theorem mtbird

Step	Hyp	Ref	Expression
1		mtbird.min	. 2 |- (ph -> -. ch)
2		mtbird.maj	. . 3 |- (ph -> (ps <-> ch))
3	2	biimpd 153	. 2 |- (ph -> (ps -> ch))
4	1, 3	mtod 108	1 |- (ph -> -. ps)

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146

This theorem is referenced by:  onsucuni2 3091  onomeneq 4519  rankr1 4674  rankxpsuc 4715  cardnn 4824  cardaleph 4885  addnidpi 5028  xrltnsymt 5550  xrlttrt 5553  zbtwnre 6221  abssubne0t 6882  hmdmadjt 9864  strlem1 10177  iintlem1 10632

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147

Copyright terms: Public domain