Theorem mtbid 327

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 251	. 2 ⊢ (𝜑 → (𝜒 → 𝜓))
4	1, 3	mtod 201	1 ⊢ (𝜑 → ¬ 𝜒)

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

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 210

This theorem is referenced by:  neleqtrd  2891  eueq3  3681  efrirr  5642  efrn2lp  5643  epne3  7772  dif1enlem  9144  ordtypelem9  9488  cantnfp1lem3  9649  cantnflem1b  9655  cantnflem1  9658  cnfcom3lem  9672  cflim2  10247  fin23lem30  10326  isf32lem5  10341  axdc3lem4  10437  axpownd  10586  pwfseqlem3  10645  grur1  10805  genpnnp  10990  xrlttri  13164  expneg  14105  bcval5  14354  seqcoll  14501  seqcoll2  14502  hashge2el2dif  14517  fsumss  15776  fprodss  16002  oddsumodd  16448  rpdvds  16718  pcmpt  16952  prmreclem2  16977  prmreclem5  16980  prmlem0  17165  sylow1lem3  19670  sylow2blem3  19692  efgredlema  19810  gsum2d2lem  20043  simpgnideld  20171  qsnzr  21452  lindsind2  21938  1stccnp  23588  kqdisj  23858  alexsubALTlem4  24176  xrhmeo  25074  minveclem3b  25556  ovolgelb  25608  volsup  25684  volsup2  25733  itg1val2  25812  itg2seq  25870  itg2cn  25891  limcnlp  26006  itgsubstlem  26176  ply1termlem  26329  radcnvlt1  26547  fsumharmonic  27142  ftalem3  27205  chpub  27350  lgsqr  27481  lgseisenlem1  27505  lgsquadlem3  27512  2sqlem8a  27555  2sqlem8  27556  2sqblem  27561  nosupbnd1lem2  27839  nosupbnd2  27846  noinfbnd1lem2  27854  noinfbnd2  27861  axtgupdim2  28706  tgdim01  28742  lnoppnhpg  29005  axcontlem2  29256  minvecolem5  31174  divnumden2  33101  mxidlirred  33700  rprmndvdsr1  33759  esplyind  33910  resssra  33922  extdgfialglem1  34027  esum2d  34428  oddpwdc  34689  eulerpartlemsv2  34693  eulerpartlemv  34699  eulerpartlemgh  34713  signslema  34894  erdszelem7  35622  erdszelem8  35623  wsuclem  36248  knoppndvlem10  37033  knoppndvlem13  37036  nlpineqsn  37977  lindsdom  38188  ftc1anclem5  38271  cntotbnd  38370  lshpdisj  39686  lcv1  39740  atlatmstc  40018  hlatcon2  40151  4noncolr3  40152  3atlem6  40187  lplnnleat  40241  lplnexllnN  40263  lvolnleat  40282  4atlem11  40308  dalem1  40358  dalemswapyzps  40389  dalemrotps  40390  2llnma1  40486  dalawlem15  40584  4atexlemcnd  40771  ltrnel  40838  cdleme15c  40975  cdleme0nex  40989  cdleme20m  41022  cdleme43bN  41189  cdleme43dN  41191  cdlemeg46nlpq  41216  cdlemg12  41349  dihmeetcN  42001  dihjatc1  42010  dihjatcclem1  42117  lclkrlem2a  42206  lcfrlem20  42261  mapdh6aN  42434  mapdh8ab  42476  hdmap1l6a  42508  aks4d1p8d1  42776  mulltgt0d  43181  mullt0b2d  43183  sn-mullt0d  43184  fimgmcyc  43229  dffltz  43293  flt4lem5a  43311  flt4lem5b  43312  flt4lem5c  43313  flt4lem5d  43314  flt4lem5e  43315  irrapxlem1  43476  elpell14qr2  43516  elpell1qr2  43526  wepwsolem  43696  fnwe2lem2  43705  brneqtrd  45723  oddfl  45924  dstregt0  45928  xrlttri5d  45930  divlt0gt0d  45932  supxrgere  45976  supxrgelem  45980  supxrge  45981  suplesup  45982  nepnfltpnf  45985  nemnftgtmnft  45987  infrpge  45994  absimnre  46117  iccdifprioo  46159  climfveq  46310  climfveqf  46321  stoweidlem34  46675  stirlinglem5  46719  dirker2re  46733  dirkerdenne0  46734  dirkertrigeq  46742  dirkercncflem2  46745  dirkercncflem4  46747  fourierdlem54  46801  elaa2lem  46874  etransclem9  46884  sge0cl  47022  sge0repnf  47027  sge0split  47050  sge0gtfsumgt  47084  mod2addne  48031  lighneallem1  48281  lighneallem3  48283  gpg3kgrtriexlem5  48776  0nodd  48859  2nodd  48861  1neven  48927