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

Theorem mpbid 145
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 142 . 2 (𝜑 → (𝜓𝜒))
41, 3mpd 13 1 (𝜑𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  mpbii  146  annimdc  879  mpbi2and  885  bilukdc  1328  equs5or  1752  eqtrd  2114  eleqtrd  2158  neeqtrd  2274  3netr3d  2278  rexlimd2  2476  ceqsalt  2626  vtoclgft  2650  vtoclegft  2671  elrab3t  2749  eueq2dc  2766  sbceq1dd  2822  csbiedf  2944  sseqtrd  3036  3sstr3d  3042  snssd  3538  dfnfc2  3627  breqtrd  3817  3brtr3d  3822  csbexga  3914  reuhypd  4229  reg2exmidlema  4285  elirr  4292  en2lp  4305  onsucuni2  4315  finds  4349  iota4  4915  iota4an  4916  funimaexglem  5013  fneu  5034  fco2  5088  fssres2  5098  fresin  5099  feu  5103  f1orescnv  5173  resdif  5179  funcocnv2  5182  f1oprg  5199  fvelrnb  5253  fimacnv  5328  f1oresrab  5361  fsn2  5369  xpsng  5370  fnressn  5381  fsnunf  5394  foeqcnvco  5461  isores1  5485  isoini2  5489  riota5f  5523  riotass2  5525  riotass  5526  ovmpt2dxf  5657  elopabi  5852  cnvf1o  5877  smores3  5942  tfrlemisucaccv  5974  tfr1onlemsucaccv  5990  tfrcllemsucaccv  6003  rdgon  6035  frecabcl  6048  frecsuclem  6055  nnsucsssuc  6136  nnsucuniel  6139  erref  6192  iserd  6198  swoer  6200  swoord1  6201  swoord2  6202  erth  6216  erthi  6218  eroveu  6263  fndmeng  6357  xpen  6386  phplem4  6390  phplem4on  6402  fidifsnen  6405  dif1en  6414  fisbth  6417  diffisn  6427  ac6sfi  6431  en2eqpr  6434  unsnfidcex  6440  unsnfidcel  6441  eqsupti  6468  supisoti  6482  ordiso2  6505  dfplpq2  6606  ltanqi  6654  ltmnqi  6655  ltaddnq  6659  subhalfnqq  6666  ltbtwnnqq  6667  archnqq  6669  prarloclemarch2  6671  enq0sym  6684  enq0ref  6685  enq0tr  6686  nqnq0pi  6690  nnnq0lem1  6698  distrnq0  6711  prarloclemlt  6745  prarloclemn  6751  prarloclemcalc  6754  genplt2i  6762  addnqprllem  6779  addnqprulem  6780  addlocprlemgt  6786  appdivnq  6815  prmuloc2  6819  ltexprlemopl  6853  ltexprlemopu  6855  ltexprlemru  6864  prplnqu  6872  cauappcvgprlemopl  6898  cauappcvgprlemlol  6899  cauappcvgprlemladdfu  6906  cauappcvgprlemladdrl  6909  cauappcvgprlem1  6911  archrecnq  6915  archrecpr  6916  caucvgprlemk  6917  caucvgprlemnbj  6919  caucvgprlemm  6920  caucvgprlemopl  6921  caucvgprlemlol  6922  caucvgprlemladdfu  6929  caucvgprlemladdrl  6930  caucvgprlem1  6931  caucvgprprlemk  6935  caucvgprprlemnkeqj  6942  caucvgprprlemnbj  6945  caucvgprprlemml  6946  caucvgprprlemmu  6947  caucvgprprlemopl  6949  caucvgprprlemlol  6950  caucvgprprlemopu  6951  caucvgprprlemexbt  6958  caucvgprprlemexb  6959  caucvgprprlem1  6961  caucvgprprlem2  6962  prsrlem1  6981  addgt0sr  7014  srpospr  7021  prsrriota  7026  caucvgsrlemgt1  7033  caucvgsrlemoffgt1  7037  caucvgsr  7040  recriota  7118  lelttr  7266  ltletr  7267  ltnsymd  7296  lensymd  7298  cnegexlem3  7352  cnegex2  7354  addcanad  7361  addcan2ad  7362  negcon1ad  7481  negne0d  7484  negrebd  7485  subeq0d  7494  subne0ad  7497  neg11d  7498  subcand  7527  subcan2d  7528  ltadd2  7590  ltadd2dd  7593  add20  7645  ltnegcon1d  7692  ltnegcon2d  7693  lenegcon1d  7694  lenegcon2d  7695  subled  7715  lesubd  7716  ltsub23d  7717  ltsub13d  7718  ltadd1dd  7723  ltsub1dd  7724  ltsub2dd  7725  leadd1dd  7726  leadd2dd  7727  lesub1dd  7728  lesub2dd  7729  recexre  7745  apreap  7754  ltmul1a  7758  reapmul1  7762  cru  7769  apreim  7770  mulge0  7786  leltap  7791  ltleap  7797  ltapd  7803  ap0gt0  7805  ap0gt0d  7806  subap0d  7807  mulcanapad  7820  mulcanap2ad  7821  eqnegad  7889  diveqap0d  7951  diveqap1d  7952  divap1d  7955  rec11apd  7965  div11apd  7984  recgt0  7995  prodgt0  7997  lemul1a  8003  lemulge12  8012  lt2msq1  8030  lediv12a  8039  recreclt  8045  nn1suc  8125  nnnlt1  8132  nn2ge  8138  nn1gt1  8139  nnrecl  8353  nn0nlt0  8381  elnn0z  8445  elz2  8500  nn0n0n1ge2b  8508  nnm1ge0  8514  nn0ge0div  8515  zextle  8519  suprzclex  8526  nn0ind-raph  8545  zindd  8546  uzneg  8718  eluzadd  8728  eluzsub  8729  uzm1  8730  uz3m2nn  8742  supminfex  8766  nn01to3  8783  ltrec1d  8875  lerec2d  8876  ledivdivd  8880  divge1  8881  ltmul1dd  8910  ltmul2dd  8911  ltdiv1dd  8912  lediv1dd  8913  ltdiv23d  8915  lediv23d  8916  nn0ledivnn  8919  addlelt  8920  xrlelttr  8952  xrltletr  8953  ixxdisj  9002  icoshftf1o  9089  icodisj  9090  lincmb01cmp  9101  iccf1o  9102  uzsubsubfz  9142  fzdisj  9147  fzopth  9155  fznatpl1  9169  fzsuc2  9172  fzp1disj  9173  fzrev2i  9179  uzdisj  9186  fseq1p1m1  9187  fzm1  9193  fzneuz  9194  fzp1nel  9197  fzrevral  9198  fznn0sub2  9216  fz0fzdiffz0  9218  difelfzle  9222  difelfznle  9223  nn0disj  9225  fzonnsub  9255  fzodisj  9264  fzouzdisj  9266  eluzgtdifelfzo  9283  ubmelfzo  9286  fzonn0p1p1  9299  ubmelm1fzo  9312  fzostep1  9323  exfzdc  9326  subfzo0  9328  qtri3or  9329  exbtwnzlemex  9336  rebtwn2z  9341  qbtwnrelemcalc  9342  qbtwnre  9343  qavgle  9345  apbtwnz  9356  flid  9366  flqwordi  9370  flqmulnn0  9381  flhalf  9384  flltdivnn0lt  9386  fldiv4p1lem1div2  9387  intfracq  9402  flqdiv  9403  flqpmodeq  9409  modqmulnn  9424  mulqaddmodid  9446  modqmuladdim  9449  modqmuladdnn0  9450  m1modge3gt1  9453  q2submod  9467  modaddmodup  9469  modqsubdir  9475  modqeqmodmin  9476  modfzo0difsn  9477  uzsinds  9518  monoord2  9552  isermono  9553  serile  9571  expival  9575  expnegap0  9581  expgt1  9611  ltexp2a  9625  le2sq2  9648  nnlesq  9675  bernneq  9690  expnbnd  9693  expnlbnd  9694  expnlbnd2  9695  expeq0d  9698  sq11d  9735  expcand  9742  nn0opthd  9746  facdiv  9762  faclbnd6  9768  facubnd  9769  facavg  9770  bcval4  9776  bcp1nk  9786  ibcval5  9787  bcpasc  9790  sizeennnuni  9803  focdmex  9811  isfinite4im  9817  sizenncl  9820  sizeunlem  9828  cjth  9871  cjdivap  9934  cjne0d  9972  cjap0d  9973  cvg1nlemcxze  10006  cvg1nlemcau  10008  cvg1nlemres  10009  recvguniq  10019  resqrexlemover  10034  resqrexlemdecn  10036  resqrexlemlo  10037  resqrexlemcalc2  10039  resqrexlemcalc3  10040  resqrexlemnmsq  10041  resqrexlemnm  10042  resqrexlemcvg  10043  resqrexlemglsq  10046  resqrexlemga  10047  leabs  10098  absrele  10107  nn0abscl  10109  ltabs  10111  abslt  10112  absle  10113  abstri  10128  amgm2  10142  sqr11d  10197  abs00d  10210  maxabsle  10228  maxabslemlub  10231  maxleastlt  10239  maxltsup  10242  minmax  10250  climi  10264  climge0  10301  climle  10310  climserile  10321  climrecvg1n  10323  fz1f1o  10336  zdvdsdc  10361  dvdstr  10377  dvdsadd2b  10387  dvdslelemd  10388  divconjdvds  10394  alzdvds  10399  dvdsext  10400  fzm1ndvds  10401  fzo0dvdseq  10402  zeo3  10412  even2n  10418  mod2eq1n2dvds  10423  nn0ehalf  10447  nnehalf  10448  nno  10450  nn0oddm1d2  10453  divalglemnqt  10464  divalglemex  10466  divalglemeuneg  10467  divalg2  10470  divalgmod  10471  flodddiv4t2lthalf  10481  zsupcllemstep  10485  infssuzex  10489  dvdsbnd  10492  gcdsupex  10493  gcdsupcl  10494  gcddvds  10499  divgcdz  10507  divgcdnn  10510  gcd0id  10514  gcdneg  10517  gcd1  10522  bezoutlemnewy  10529  bezoutlemstep  10530  bezoutlemmo  10539  bezoutlemsup  10542  dfgcd3  10543  bezout  10544  dfgcd2  10547  mulgcd  10549  sqgcd  10562  dvdssqlem  10563  bezoutr1  10566  lcmval  10589  lcmcllem  10593  dvdslcm  10595  lcmgcdlem  10603  lcmdvds  10605  lcmgcdeq  10609  ncoprmgcdne1b  10615  mulgcddvds  10620  rpmulgcd2  10621  qredeu  10623  rpdvds  10625  prmind2  10646  nprm  10649  dvdsnprmd  10651  divgcdodd  10666  isprm6  10670  prmexpb  10674  pw2dvds  10688  pw2dvdseulemle  10689  oddpwdclemdc  10695  sqne2sq  10699  znege1  10700  sqrt2irraplemnn  10701  oddennn  10703
  Copyright terms: Public domain W3C validator