Theorem mtbid 316

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

Hypotheses

Ref	Expression
mtbid.min	⊢ (𝜑 → ¬ 𝜓)
mtbid.maj	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
mtbid	⊢ (𝜑 → ¬ 𝜒)

Proof of Theorem mtbid

Step	Hyp	Ref	Expression
1		mtbid.min	. 2 ⊢ (𝜑 → ¬ 𝜓)
2		mtbid.maj	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	2	biimprd 240	. 2 ⊢ (𝜑 → (𝜒 → 𝜓))
4	1, 3	mtod 190	1 ⊢ (𝜑 → ¬ 𝜒)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198

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 199

This theorem is referenced by:  sylnib  320  neleqtrd  2880  eueq3  3593  efrirr  5336  efrn2lp  5337  epne3  7258  wfrlem10  7707  ordtypelem9  8720  cantnfp1lem3  8874  cantnflem1b  8880  cantnflem1  8883  cnfcom3lem  8897  cflim2  9420  fin23lem30  9499  isf32lem5  9514  axdc3lem4  9610  axpownd  9758  pwfseqlem3  9817  grur1  9977  genpnnp  10162  xrlttri  12282  expneg  13186  bcval5  13423  seqcoll  13562  seqcoll2  13563  hashge2el2dif  13576  fsumss  14863  fprodss  15081  oddsumodd  15520  rpdvds  15779  pcmpt  16000  prmreclem2  16025  prmreclem5  16028  prmlem0  16211  sylow1lem3  18399  sylow2blem3  18421  efgredlema  18538  gsum2d2lem  18758  lindsind2  20562  1stccnp  21674  kqdisj  21944  alexsubALTlem4  22262  xrhmeo  23153  minveclem3b  23634  ovolgelb  23684  volsup  23760  volsup2  23809  itg1val2  23888  itg2seq  23946  itg2cn  23967  limcnlp  24079  itgsubstlem  24248  ply1termlem  24396  radcnvlt1  24609  fsumharmonic  25190  ftalem3  25253  chpub  25397  lgsqr  25528  lgseisenlem1  25552  lgsquadlem3  25559  2sqlem8a  25602  2sqlem8  25603  2sqblem  25608  tgdim01  25858  lnoppnhpg  26112  acopyeu  26183  axcontlem2  26314  minvecolem5  28309  divnumden2  30128  esum2d  30753  oddpwdc  31014  eulerpartlemsv2  31018  eulerpartlemv  31024  eulerpartlemgh  31038  signslema  31239  erdszelem7  31778  erdszelem8  31779  wsuclem  32359  nosupbnd1lem2  32444  nosupbnd2  32451  knoppndvlem10  33094  knoppndvlem13  33097  lindsdom  34029  ftc1anclem5  34114  cntotbnd  34219  lshpdisj  35141  lcv1  35195  atlatmstc  35473  hlatcon2  35606  4noncolr3  35607  3atlem6  35642  lplnnleat  35696  lplnexllnN  35718  lvolnleat  35737  4atlem11  35763  dalem1  35813  dalemswapyzps  35844  dalemrotps  35845  2llnma1  35941  dalawlem15  36039  4atexlemcnd  36226  ltrnel  36293  cdleme15c  36430  cdleme0nex  36444  cdleme20m  36477  cdleme43bN  36644  cdleme43dN  36646  cdlemeg46nlpq  36671  cdlemg12  36804  dihmeetcN  37456  dihjatc1  37465  dihjatcclem1  37572  lclkrlem2a  37661  lcfrlem20  37716  mapdh6aN  37889  mapdh8ab  37931  hdmap1l6a  37963  dffltz  38213  irrapxlem1  38346  elpell14qr2  38386  elpell1qr2  38396  wepwsolem  38571  fnwe2lem2  38580  brneqtrd  40179  oddfl  40399  dstregt0  40403  xrlttri5d  40405  divlt0gt0d  40408  supxrgere  40457  supxrgelem  40461  supxrge  40462  suplesup  40463  nepnfltpnf  40466  nemnftgtmnft  40468  infrpge  40475  absimnre  40612  iccdifprioo  40651  climfveq  40809  climfveqf  40820  stoweidlem34  41178  stirlinglem5  41222  dirker2re  41236  dirkerdenne0  41237  dirkertrigeq  41245  dirkercncflem2  41248  dirkercncflem4  41250  fourierdlem54  41304  elaa2lem  41377  etransclem9  41387  sge0cl  41522  sge0repnf  41527  sge0split  41550  sge0gtfsumgt  41584  lighneallem1  42543  lighneallem3  42545  0nodd  42825  2nodd  42827  1neven  42947