Theorem mtbid 673

Description: A deduction from a biconditional, similar to modus tollens. (Contributed by NM, 26-Nov-1995.)

Hypotheses

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

Assertion

Ref	Expression
mtbid	|- ( ph -> -. ch )

Proof of Theorem mtbid

Step	Hyp	Ref	Expression
1		mtbid.min	. 2 |- ( ph -> -. ps )
2		mtbid.maj	. . 3 |- ( ph -> ( ps <-> ch ) )
3	2	biimprd 158	. 2 |- ( ph -> ( ch -> ps ) )
4	1, 3	mtod 664	1 |- ( ph -> -. ch )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylnib  677  eqneltrrd  2286  neleqtrd  2287  eueq3dc  2926  efrirr  4368  fidcenumlemrks  6977  nqnq0pi  7462  zdclt  9355  xleaddadd  9912  frec2uzf1od  10432  expnegap0  10554  bcval5  10770  zfz1isolemiso  10846  seq3coll  10849  fisumss  11427  fprodssdc  11625  rpdvds  12126  oddpwdclemodd  12199  pceq0  12349  pcmpt  12370  lgseisenlem1  14887  2sqlem8a  14906  2sqlem8  14907  pwle2  15186