ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpbid GIF version

Theorem mpbid 135
Description: A deduction from a biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
mpbid.min (𝜑𝜓)
mpbid.maj (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
mpbid (𝜑𝜒)

Proof of Theorem mpbid
StepHypRef Expression
1 mpbid.min . 2 (𝜑𝜓)
2 mpbid.maj . . 3 (𝜑 → (𝜓𝜒))
32biimpd 132 . 2 (𝜑 → (𝜓𝜒))
41, 3mpd 13 1 (𝜑𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  mpbii  136  annimdc  845  mpbi2and  850  bilukdc  1287  equs5or  1711  eqtrd  2072  eleqtrd  2116  neeqtrd  2233  3netr3d  2237  rexlimd2  2431  ceqsalt  2580  vtoclgft  2604  vtoclegft  2625  elrab3t  2697  eueq2dc  2714  sbceq1dd  2770  csbiedf  2887  sseqtrd  2981  3sstr3d  2987  snssd  3509  dfnfc2  3598  breqtrd  3788  3brtr3d  3793  csbexga  3885  reuhypd  4203  reg2exmidlema  4259  elirr  4266  en2lp  4278  onsucuni2  4288  finds  4323  iota4  4885  iota4an  4886  funimaexglem  4982  fneu  5003  fco2  5057  fssres2  5067  fresin  5068  feu  5072  f1orescnv  5142  resdif  5148  funcocnv2  5151  f1oprg  5168  fvelrnb  5221  fimacnv  5296  f1oresrab  5329  fsn2  5337  xpsng  5338  fnressn  5349  fsnunf  5362  foeqcnvco  5430  isores1  5454  isoini2  5458  riota5f  5492  riotass2  5494  riotass  5495  ovmpt2dxf  5626  elopabi  5821  cnvf1o  5846  smores3  5908  tfrlemisucaccv  5939  nnsucsssuc  6071  erref  6126  iserd  6132  swoer  6134  swoord1  6135  swoord2  6136  erth  6150  erthi  6152  eroveu  6197  fndmeng  6289  phplem4  6318  phplem4on  6329  fidifsnen  6331  dif1en  6337  fisbth  6340  diffisn  6350  ac6sfi  6352  ordiso2  6355  dfplpq2  6450  ltanqi  6498  ltmnqi  6499  ltaddnq  6503  subhalfnqq  6510  ltbtwnnqq  6511  archnqq  6513  prarloclemarch2  6515  enq0sym  6528  enq0ref  6529  enq0tr  6530  nqnq0pi  6534  nnnq0lem1  6542  distrnq0  6555  prarloclemlt  6589  prarloclemn  6595  prarloclemcalc  6598  genplt2i  6606  addnqprllem  6623  addnqprulem  6624  addlocprlemgt  6630  appdivnq  6659  prmuloc2  6663  ltexprlemopl  6697  ltexprlemopu  6699  ltexprlemru  6708  prplnqu  6716  cauappcvgprlemopl  6742  cauappcvgprlemlol  6743  cauappcvgprlemladdfu  6750  cauappcvgprlemladdrl  6753  cauappcvgprlem1  6755  archrecnq  6759  archrecpr  6760  caucvgprlemk  6761  caucvgprlemnbj  6763  caucvgprlemm  6764  caucvgprlemopl  6765  caucvgprlemlol  6766  caucvgprlemladdfu  6773  caucvgprlemladdrl  6774  caucvgprlem1  6775  caucvgprprlemk  6779  caucvgprprlemnkeqj  6786  caucvgprprlemnbj  6789  caucvgprprlemml  6790  caucvgprprlemmu  6791  caucvgprprlemopl  6793  caucvgprprlemlol  6794  caucvgprprlemopu  6795  caucvgprprlemexbt  6802  caucvgprprlemexb  6803  caucvgprprlem1  6805  caucvgprprlem2  6806  prsrlem1  6825  addgt0sr  6858  srpospr  6865  prsrriota  6870  caucvgsrlemgt1  6877  caucvgsrlemoffgt1  6881  caucvgsr  6884  recriota  6962  lelttr  7104  ltletr  7105  ltnsymd  7134  cnegexlem3  7186  cnegex2  7188  addcanad  7195  addcan2ad  7196  negcon1ad  7315  negne0d  7318  negrebd  7319  subeq0d  7328  subne0ad  7331  neg11d  7332  subcand  7361  subcan2d  7362  ltadd2  7414  ltadd2dd  7417  add20  7467  ltnegcon1d  7514  ltnegcon2d  7515  lenegcon1d  7516  lenegcon2d  7517  subled  7537  lesubd  7538  ltsub23d  7539  ltsub13d  7540  ltadd1dd  7545  ltsub1dd  7546  ltsub2dd  7547  leadd1dd  7548  leadd2dd  7549  lesub1dd  7550  lesub2dd  7551  recexre  7567  apreap  7576  ltmul1a  7580  reapmul1  7584  cru  7591  apreim  7592  mulge0  7608  leltap  7613  ltleap  7619  ltapd  7625  ap0gt0  7627  ap0gt0d  7628  subap0d  7629  mulcanapad  7642  mulcanap2ad  7643  eqnegad  7708  diveqap0d  7770  diveqap1d  7771  divap1d  7774  rec11apd  7784  div11apd  7803  recgt0  7814  prodgt0  7816  lemul1a  7822  lemulge12  7831  lt2msq1  7849  lediv12a  7858  recreclt  7864  nn1suc  7931  nnnlt1  7938  nn2ge  7944  nn1gt1  7945  nnrecl  8177  nn0nlt0  8206  elnn0z  8256  elz2  8310  nn0n0n1ge2b  8318  nnm1ge0  8324  nn0ge0div  8325  zextle  8329  nn0ind-raph  8353  zindd  8354  uzneg  8489  eluzadd  8499  eluzsub  8500  uzm1  8501  uz3m2nn  8513  nn01to3  8550  ltrec1d  8641  lerec2d  8642  ledivdivd  8646  divge1  8647  ltmul1dd  8676  ltmul2dd  8677  ltdiv1dd  8678  lediv1dd  8679  ltdiv23d  8681  lediv23d  8682  xrlelttr  8720  xrltletr  8721  ixxdisj  8770  icoshftf1o  8857  icodisj  8858  lincmb01cmp  8869  iccf1o  8870  uzsubsubfz  8909  fzdisj  8914  fzopth  8922  fznatpl1  8936  fzsuc2  8939  fzp1disj  8940  fzrev2i  8946  uzdisj  8953  fseq1p1m1  8954  fzm1  8960  fzneuz  8961  fzp1nel  8964  fzrevral  8965  elfz0addOLD  8978  fznn0sub2  8983  fz0fzdiffz0  8985  difelfzle  8990  difelfznle  8991  nn0disj  8993  fzonnsub  9023  fzodisj  9032  fzouzdisj  9034  eluzgtdifelfzo  9051  ubmelfzo  9054  fzonn0p1p1  9067  ubmelm1fzo  9080  fzostep1  9091  subfzo0  9095  qtri3or  9096  qbtwnzlemex  9103  rebtwn2z  9107  qbtwnrelemcalc  9108  qbtwnre  9109  flid  9124  flqwordi  9128  flqmulnn0  9139  flhalf  9142  flltdivnn0lt  9144  fldiv4p1lem1div2  9145  monoord2  9210  isermono  9211  serile  9227  expival  9231  expnegap0  9237  expgt1  9267  ltexp2a  9280  le2sq2  9303  nnlesq  9330  bernneq  9343  expnbnd  9346  expnlbnd  9347  expnlbnd2  9348  expeq0d  9351  sq11d  9387  cjth  9420  cjdivap  9483  cjne0d  9521  cjap0d  9522  cvg1nlemcxze  9555  cvg1nlemcau  9557  cvg1nlemres  9558  recvguniq  9567  resqrexlemover  9582  resqrexlemdecn  9584  resqrexlemlo  9585  resqrexlemcalc2  9587  resqrexlemcalc3  9588  resqrexlemnmsq  9589  resqrexlemnm  9590  resqrexlemcvg  9591  resqrexlemglsq  9594  resqrexlemga  9595  leabs  9646  absrele  9653  nn0abscl  9655  ltabs  9657  abslt  9658  absle  9659  abstri  9674  amgm2  9688  sqr11d  9743  abs00d  9756  climi  9782  climge0  9819  climle  9828  climserile  9839  climrecvg1n  9841
  Copyright terms: Public domain W3C validator