Theorem mtbiri 719

Description: An inference from a biconditional, similar to modus tollens.

Hypotheses

Ref	Expression
mtbiri.min	⊢ ¬ χ
mtbiri.maj	⊢ (φ → (ψ ↔ χ))

Assertion

Ref	Expression
mtbiri	⊢ (φ → ¬ ψ)

Proof of Theorem mtbiri

Step	Hyp	Ref	Expression
1		mtbiri.min	. 2 ⊢ ¬ χ
2		mtbiri.maj	. . 3 ⊢ (φ → (ψ ↔ χ))
3	2	biimpd 153	. 2 ⊢ (φ → (ψ → χ))
4	1, 3	mtoi 107	1 ⊢ (φ → ¬ ψ)

Syntax hints:  ¬ wn 2   → wi 3   ↔ wb 146

This theorem is referenced by:  psstr 2153  n0i 2288  disjsn 2445  axnul 2714  intex 2734  intnex 2735  iin0 2745  0ellim 3037  ordunisuc 3095  dflim3 3124  vtoclibr 3219  onxpdisj 3247  fn0 3611  fvprc 3727  ndmfvrcl 3752  fvopabn 3792  dfrdg2 3939  oprssdm 4048  ndmoprrcl 4052  ecelqsdm 4305  2dom 4433  sdomex 4479  sucprcreg 4609  preleq 4612  omelon 4638  rankr1 4684  rankxpsuc 4725  card1 4843  sdomsdomcard 4859  alephnbtwn2 4880  alephgeom 4893  alephval2 4913  alephval3 4914  cfsuc 4927  ltrpq 5097  ltsopr 5148  ltapr 5163  ltxrltt 5512  xrltnrt 5553  pnfnltt 5558  nltmnft 5559  xrltnsymt 5562  nltpnftt 5578  ngtmnftt 5579  nnne0t 5951  xrsupsslem 6078  xrinfmsslem 6079  xrub 6082  zneo 6202  qbtwnxr 6280  eliooret 6387  sqrlem13 6686  ivthlem7 7287  tpsex 7606  vcex 8195  nvex 8226  spwnex3 8651  efif1lem5 8729  norm1ex 9117  dmadjrnb 9825  strlem1 10172  large 10189

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