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

Theorem mpbid 139
Description: A deduction from a biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
mpbid.min  |-  ( ph  ->  ps )
mpbid.maj  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
mpbid  |-  ( ph  ->  ch )

Proof of Theorem mpbid
StepHypRef Expression
1 mpbid.min . 2  |-  ( ph  ->  ps )
2 mpbid.maj . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
32biimpd 136 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41, 3mpd 13 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  mpbii  140  annimdc  856  mpbi2and  861  bilukdc  1303  equs5or  1727  eqtrd  2088  eleqtrd  2132  neeqtrd  2248  3netr3d  2252  rexlimd2  2448  ceqsalt  2597  vtoclgft  2621  vtoclegft  2642  elrab3t  2720  eueq2dc  2737  sbceq1dd  2793  csbiedf  2915  sseqtrd  3009  3sstr3d  3015  snssd  3537  dfnfc2  3626  breqtrd  3816  3brtr3d  3821  csbexga  3913  reuhypd  4231  reg2exmidlema  4287  elirr  4294  en2lp  4306  onsucuni2  4316  finds  4351  iota4  4913  iota4an  4914  funimaexglem  5010  fneu  5031  fco2  5085  fssres2  5095  fresin  5096  feu  5100  f1orescnv  5170  resdif  5176  funcocnv2  5179  f1oprg  5196  fvelrnb  5249  fimacnv  5324  f1oresrab  5357  fsn2  5365  xpsng  5366  fnressn  5377  fsnunf  5390  foeqcnvco  5458  isores1  5482  isoini2  5486  riota5f  5520  riotass2  5522  riotass  5523  ovmpt2dxf  5654  elopabi  5849  cnvf1o  5874  smores3  5939  tfrlemisucaccv  5970  nnsucsssuc  6102  erref  6157  iserd  6163  swoer  6165  swoord1  6166  swoord2  6167  erth  6181  erthi  6183  eroveu  6228  fndmeng  6320  phplem4  6349  phplem4on  6360  fidifsnen  6362  dif1en  6368  fisbth  6371  diffisn  6381  ac6sfi  6383  eqsupti  6402  supisoti  6414  ordiso2  6415  dfplpq2  6510  ltanqi  6558  ltmnqi  6559  ltaddnq  6563  subhalfnqq  6570  ltbtwnnqq  6571  archnqq  6573  prarloclemarch2  6575  enq0sym  6588  enq0ref  6589  enq0tr  6590  nqnq0pi  6594  nnnq0lem1  6602  distrnq0  6615  prarloclemlt  6649  prarloclemn  6655  prarloclemcalc  6658  genplt2i  6666  addnqprllem  6683  addnqprulem  6684  addlocprlemgt  6690  appdivnq  6719  prmuloc2  6723  ltexprlemopl  6757  ltexprlemopu  6759  ltexprlemru  6768  prplnqu  6776  cauappcvgprlemopl  6802  cauappcvgprlemlol  6803  cauappcvgprlemladdfu  6810  cauappcvgprlemladdrl  6813  cauappcvgprlem1  6815  archrecnq  6819  archrecpr  6820  caucvgprlemk  6821  caucvgprlemnbj  6823  caucvgprlemm  6824  caucvgprlemopl  6825  caucvgprlemlol  6826  caucvgprlemladdfu  6833  caucvgprlemladdrl  6834  caucvgprlem1  6835  caucvgprprlemk  6839  caucvgprprlemnkeqj  6846  caucvgprprlemnbj  6849  caucvgprprlemml  6850  caucvgprprlemmu  6851  caucvgprprlemopl  6853  caucvgprprlemlol  6854  caucvgprprlemopu  6855  caucvgprprlemexbt  6862  caucvgprprlemexb  6863  caucvgprprlem1  6865  caucvgprprlem2  6866  prsrlem1  6885  addgt0sr  6918  srpospr  6925  prsrriota  6930  caucvgsrlemgt1  6937  caucvgsrlemoffgt1  6941  caucvgsr  6944  recriota  7022  lelttr  7165  ltletr  7166  ltnsymd  7195  lensymd  7197  cnegexlem3  7251  cnegex2  7253  addcanad  7260  addcan2ad  7261  negcon1ad  7380  negne0d  7383  negrebd  7384  subeq0d  7393  subne0ad  7396  neg11d  7397  subcand  7426  subcan2d  7427  ltadd2  7488  ltadd2dd  7491  add20  7543  ltnegcon1d  7590  ltnegcon2d  7591  lenegcon1d  7592  lenegcon2d  7593  subled  7613  lesubd  7614  ltsub23d  7615  ltsub13d  7616  ltadd1dd  7621  ltsub1dd  7622  ltsub2dd  7623  leadd1dd  7624  leadd2dd  7625  lesub1dd  7626  lesub2dd  7627  recexre  7643  apreap  7652  ltmul1a  7656  reapmul1  7660  cru  7667  apreim  7668  mulge0  7684  leltap  7689  ltleap  7695  ltapd  7701  ap0gt0  7703  ap0gt0d  7704  subap0d  7705  mulcanapad  7718  mulcanap2ad  7719  eqnegad  7785  diveqap0d  7847  diveqap1d  7848  divap1d  7851  rec11apd  7861  div11apd  7880  recgt0  7891  prodgt0  7893  lemul1a  7899  lemulge12  7908  lt2msq1  7926  lediv12a  7935  recreclt  7941  nn1suc  8009  nnnlt1  8016  nn2ge  8022  nn1gt1  8023  nnrecl  8237  nn0nlt0  8265  elnn0z  8315  elz2  8370  nn0n0n1ge2b  8378  nnm1ge0  8384  nn0ge0div  8385  zextle  8389  nn0ind-raph  8414  zindd  8415  uzneg  8587  eluzadd  8597  eluzsub  8598  uzm1  8599  uz3m2nn  8611  nn01to3  8649  ltrec1d  8741  lerec2d  8742  ledivdivd  8746  divge1  8747  ltmul1dd  8776  ltmul2dd  8777  ltdiv1dd  8778  lediv1dd  8779  ltdiv23d  8781  lediv23d  8782  nn0ledivnn  8785  addlelt  8786  xrlelttr  8823  xrltletr  8824  ixxdisj  8873  icoshftf1o  8960  icodisj  8961  lincmb01cmp  8972  iccf1o  8973  uzsubsubfz  9013  fzdisj  9018  fzopth  9026  fznatpl1  9040  fzsuc2  9043  fzp1disj  9044  fzrev2i  9050  uzdisj  9057  fseq1p1m1  9058  fzm1  9064  fzneuz  9065  fzp1nel  9068  fzrevral  9069  elfz0addOLD  9082  fznn0sub2  9087  fz0fzdiffz0  9089  difelfzle  9094  difelfznle  9095  nn0disj  9097  fzonnsub  9127  fzodisj  9136  fzouzdisj  9138  eluzgtdifelfzo  9155  ubmelfzo  9158  fzonn0p1p1  9171  ubmelm1fzo  9184  fzostep1  9195  subfzo0  9199  qtri3or  9200  qbtwnzlemex  9207  rebtwn2z  9211  qbtwnrelemcalc  9212  qbtwnre  9213  qavgle  9215  flid  9234  flqwordi  9238  flqmulnn0  9249  flhalf  9252  flltdivnn0lt  9254  fldiv4p1lem1div2  9255  intfracq  9270  flqdiv  9271  flqpmodeq  9277  modqmulnn  9292  mulqaddmodid  9314  modqmuladdim  9317  modqmuladdnn0  9318  m1modge3gt1  9321  q2submod  9335  modaddmodup  9337  modqsubdir  9343  modqeqmodmin  9344  modfzo0difsn  9345  monoord2  9400  isermono  9401  serile  9418  expival  9422  expnegap0  9428  expgt1  9458  ltexp2a  9472  le2sq2  9495  nnlesq  9522  bernneq  9537  expnbnd  9540  expnlbnd  9541  expnlbnd2  9542  expeq0d  9545  sq11d  9582  nn0opthd  9590  facdiv  9606  faclbnd6  9612  facubnd  9613  facavg  9614  bcval4  9620  bcp1nk  9630  ibcval5  9631  bcpasc  9634  cjth  9674  cjdivap  9737  cjne0d  9775  cjap0d  9776  cvg1nlemcxze  9809  cvg1nlemcau  9811  cvg1nlemres  9812  recvguniq  9822  resqrexlemover  9837  resqrexlemdecn  9839  resqrexlemlo  9840  resqrexlemcalc2  9842  resqrexlemcalc3  9843  resqrexlemnmsq  9844  resqrexlemnm  9845  resqrexlemcvg  9846  resqrexlemglsq  9849  resqrexlemga  9850  leabs  9901  absrele  9910  nn0abscl  9912  ltabs  9914  abslt  9915  absle  9916  abstri  9931  amgm2  9945  sqr11d  10000  abs00d  10013  climi  10039  climge0  10076  climle  10085  climserile  10096  climrecvg1n  10098  dvdstr  10144  dvdsadd2b  10154  dvdslelemd  10155  divconjdvds  10161  alzdvds  10166  dvdsext  10167  fzm1ndvds  10168  fzo0dvdseq  10169  zeo3  10179  even2n  10185  mod2eq1n2dvds  10191  nn0ehalf  10215  nnehalf  10216  nno  10218  nn0oddm1d2  10221  divalglemnqt  10232  divalglemex  10234  divalglemeuneg  10235  divalg2  10238  divalgmod  10239  flodddiv4t2lthalf  10249  pw2dvds  10254  pw2dvdseulemle  10255  oddpwdclemdc  10261
  Copyright terms: Public domain W3C validator