MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mtbid Structured version   Visualization version   GIF version

Theorem mtbid 313
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
StepHypRef Expression
1 mtbid.min . 2 (𝜑 → ¬ 𝜓)
2 mtbid.maj . . 3 (𝜑 → (𝜓𝜒))
32biimprd 238 . 2 (𝜑 → (𝜒𝜓))
41, 3mtod 189 1 (𝜑 → ¬ 𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196
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 197
This theorem is referenced by:  sylnib  317  neleqtrd  2751  eueq3  3414  efrirr  5124  efrn2lp  5125  epne3  7022  wfrlem10  7469  ordtypelem9  8472  cantnfp1lem3  8615  cantnflem1b  8621  cantnflem1  8624  cnfcom3lem  8638  cflim2  9123  fin23lem30  9202  isf32lem5  9217  axdc3lem4  9313  axpownd  9461  pwfseqlem3  9520  grur1  9680  genpnnp  9865  xrlttri  12010  expneg  12908  bcval5  13145  seqcoll  13286  seqcoll2  13287  hashge2el2dif  13300  fsumss  14500  fprodss  14722  oddsumodd  15160  rpdvds  15421  pcmpt  15643  prmreclem2  15668  prmreclem5  15671  prmlem0  15859  sylow1lem3  18061  sylow2blem3  18083  efgredlema  18199  gsum2d2lem  18418  lindsind2  20206  1stccnp  21313  kqdisj  21583  alexsubALTlem4  21901  xrhmeo  22792  minveclem3b  23245  ovolgelb  23294  volsup  23370  volsup2  23419  itg1val2  23496  itg2seq  23554  itg2cn  23575  limcnlp  23687  itgsubstlem  23856  ply1termlem  24004  radcnvlt1  24217  fsumharmonic  24783  ftalem3  24846  chpub  24990  lgsqr  25121  lgseisenlem1  25145  lgsquadlem3  25152  2sqlem8a  25195  2sqlem8  25196  2sqblem  25201  tgdim01  25447  lnoppnhpg  25701  acopyeu  25770  axcontlem2  25890  minvecolem5  27865  divnumden2  29692  esum2d  30283  oddpwdc  30544  eulerpartlemsv2  30548  eulerpartlemv  30554  eulerpartlemgh  30568  signslema  30767  erdszelem7  31305  erdszelem8  31306  wsuclem  31895  nosupbnd1lem2  31980  nosupbnd2  31987  knoppndvlem10  32637  knoppndvlem13  32640  lindsdom  33533  ftc1anclem5  33619  cntotbnd  33725  lshpdisj  34592  lcv1  34646  atlatmstc  34924  hlatcon2  35056  4noncolr3  35057  3atlem6  35092  lplnnleat  35146  lplnexllnN  35168  lvolnleat  35187  4atlem11  35213  dalem1  35263  dalemswapyzps  35294  dalemrotps  35295  2llnma1  35391  dalawlem15  35489  4atexlemcnd  35676  ltrnel  35743  cdleme15c  35881  cdleme0nex  35895  cdleme20m  35928  cdleme43bN  36095  cdleme43dN  36097  cdlemeg46nlpq  36122  cdlemg12  36255  dihmeetcN  36908  dihjatc1  36917  dihjatcclem1  37024  lclkrlem2a  37113  lcfrlem20  37168  mapdh6aN  37341  mapdh8ab  37383  hdmap1l6a  37416  irrapxlem1  37703  elpell14qr2  37743  elpell1qr2  37753  wepwsolem  37929  fnwe2lem2  37938  brneqtrd  39562  oddfl  39803  dstregt0  39807  xrlttri5d  39809  divlt0gt0d  39812  supxrgere  39862  supxrgelem  39866  supxrge  39867  suplesup  39868  nepnfltpnf  39871  nemnftgtmnft  39873  infrpge  39880  absimnre  40020  iccdifprioo  40060  climfveq  40219  climfveqf  40230  stoweidlem34  40569  stirlinglem5  40613  dirker2re  40627  dirkerdenne0  40628  dirkertrigeq  40636  dirkercncflem2  40639  dirkercncflem4  40641  fourierdlem54  40695  elaa2lem  40768  etransclem9  40778  sge0cl  40916  sge0repnf  40921  sge0split  40944  sge0gtfsumgt  40978  lighneallem1  41847  lighneallem3  41849  0nodd  42135  2nodd  42137  1neven  42257
  Copyright terms: Public domain W3C validator