Theorem mpbid 146

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

Step	Hyp	Ref	Expression
1		mpbid.min	. 2 |- ( ph -> ps )
2		mpbid.maj	. . 3 |- ( ph -> ( ps <-> ch ) )
3	2	biimpd 143	. 2 |- ( ph -> ( ps -> ch ) )
4	1, 3	mpd 13	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mpbii  147  annimdc  922  mpbi2and  928  bilukdc  1378  equs5or  1810  eqtrd  2190  eleqtrd  2236  neeqtrd  2355  3netr3d  2359  rexlimd2  2572  ceqsalt  2738  vtoclgft  2762  vtoclegft  2784  elrab3t  2867  eueq2dc  2885  sbceq1dd  2943  csbiedf  3071  sseqtrd  3166  3sstr3d  3172  ifbothdadc  3537  snssd  3703  dfnfc2  3792  breqdi  3982  breqtrd  3992  3brtr3d  3997  csbexga  4094  reuhypd  4433  reg2exmidlema  4495  elirr  4502  en2lp  4515  onsucuni2  4525  finds  4561  iota4  5155  iota4an  5156  funimaexglem  5255  fneu  5276  fco2  5338  fssres2  5349  fresin  5350  feu  5354  f1orescnv  5432  resdif  5438  funcocnv2  5441  f1oprg  5460  fvelrnb  5518  fimacnv  5598  f1oresrab  5634  fsn2  5643  xpsng  5644  fnressn  5655  fsnunf  5669  foeqcnvco  5742  isores1  5766  isoini2  5771  riota5f  5806  riotass2  5808  riotass  5809  ovmpodxf  5948  elopabi  6145  cnvf1o  6174  smores3  6242  tfrlemisucaccv  6274  tfr1onlemsucaccv  6290  tfrcllemsucaccv  6303  rdgon  6335  frecabcl  6348  frecsuclem  6355  nnsucsssuc  6441  nnsucuniel  6444  erref  6502  iserd  6508  swoer  6510  swoord1  6511  swoord2  6512  erth  6526  erthi  6528  eroveu  6573  pmresg  6623  mapsn  6637  fndmeng  6757  xpen  6792  phplem4  6802  phplem4on  6814  fidifsnen  6817  dif1en  6826  dif1enen  6827  fisbth  6830  diffisn  6840  ac6sfi  6845  fimax2gtri  6848  en2eqpr  6854  unsnfidcex  6866  unsnfidcel  6867  fiintim  6875  fidcenumlemrks  6899  elfi2  6918  elfir  6919  fiuni  6924  fifo  6926  eqsupti  6942  supisoti  6956  ordiso2  6981  casef  7034  difinfsnlem  7045  ctmlemr  7054  ctssdccl  7057  enumct  7061  nnnninfeq  7073  nnnninfeq2  7074  enomnilem  7083  exmidomni  7087  fodjum  7091  fodjuomnilemres  7093  mkvprop  7103  enmkvlem  7106  enwomnilem  7114  acfun  7144  ccfunen  7186  cc2lem  7188  dfplpq2  7276  ltanqi  7324  ltmnqi  7325  ltaddnq  7329  subhalfnqq  7336  ltbtwnnqq  7337  archnqq  7339  prarloclemarch2  7341  enq0sym  7354  enq0ref  7355  enq0tr  7356  nqnq0pi  7360  nnnq0lem1  7368  distrnq0  7381  prarloclemlt  7415  prarloclemn  7421  prarloclemcalc  7424  genplt2i  7432  addnqprllem  7449  addnqprulem  7450  addlocprlemgt  7456  appdivnq  7485  prmuloc2  7489  ltexprlemopl  7523  ltexprlemopu  7525  ltexprlemru  7534  prplnqu  7542  cauappcvgprlemopl  7568  cauappcvgprlemlol  7569  cauappcvgprlemladdfu  7576  cauappcvgprlemladdrl  7579  cauappcvgprlem1  7581  archrecnq  7585  archrecpr  7586  caucvgprlemk  7587  caucvgprlemnbj  7589  caucvgprlemm  7590  caucvgprlemopl  7591  caucvgprlemlol  7592  caucvgprlemladdfu  7599  caucvgprlemladdrl  7600  caucvgprlem1  7601  caucvgprprlemk  7605  caucvgprprlemnkeqj  7612  caucvgprprlemnbj  7615  caucvgprprlemml  7616  caucvgprprlemmu  7617  caucvgprprlemopl  7619  caucvgprprlemlol  7620  caucvgprprlemopu  7621  caucvgprprlemexbt  7628  caucvgprprlemexb  7629  caucvgprprlem1  7631  caucvgprprlem2  7632  suplocexprlemru  7641  suplocexprlemdisj  7642  suplocexprlemloc  7643  suplocexprlemub  7645  suplocexprlemlub  7646  prsrlem1  7664  addgt0sr  7697  srpospr  7705  prsrriota  7710  caucvgsrlemgt1  7717  caucvgsrlemoffgt1  7721  caucvgsr  7724  mappsrprg  7726  suplocsrlemb  7728  suplocsrlempr  7729  suplocsrlem  7730  recriota  7812  axsuploc  7952  lelttr  7968  ltletr  7969  ltnsymd  7999  lensymd  8001  cnegexlem3  8056  cnegex2  8058  addcanad  8065  addcan2ad  8066  negcon1ad  8185  negne0d  8188  negrebd  8189  subeq0d  8198  subne0ad  8201  neg11d  8202  subcand  8231  subcan2d  8232  ltadd2  8298  ltadd2dd  8301  add20  8353  ltnegcon1d  8404  ltnegcon2d  8405  lenegcon1d  8406  lenegcon2d  8407  subled  8427  lesubd  8428  ltsub23d  8429  ltsub13d  8430  ltadd1dd  8435  ltsub1dd  8436  ltsub2dd  8437  leadd1dd  8438  leadd2dd  8439  lesub1dd  8440  lesub2dd  8441  recexre  8457  apreap  8466  ltmul1a  8470  reapmul1  8474  cru  8481  apreim  8482  mulge0  8498  leltap  8504  negap0d  8510  ltleap  8511  ltapd  8517  ap0gt0  8519  ap0gt0d  8520  mulcanapad  8541  mulcanap2ad  8542  eqnegad  8611  diveqap0d  8674  diveqap1d  8675  divap1d  8678  rec11apd  8688  div11apd  8708  div2subap  8714  recgt0  8726  prodgt0  8728  lemul1a  8734  lemulge12  8743  lt2msq1  8761  lediv12a  8770  recreclt  8776  nn1suc  8857  nnnlt1  8864  nn2ge  8871  nn1gt1  8872  nnrecl  9093  nn0nlt0  9121  elnn0z  9185  elz2  9240  nn0n0n1ge2b  9248  nnm1ge0  9255  nn0ge0div  9256  zextle  9260  suprzclex  9267  nn0ind-raph  9286  zindd  9287  uzneg  9462  eluzadd  9472  eluzsub  9473  uzm1  9474  uz3m2nn  9489  supminfex  9513  infregelbex  9514  nn01to3  9532  ltrec1d  9630  lerec2d  9631  ledivdivd  9635  divge1  9636  ltmul1dd  9665  ltmul2dd  9666  ltdiv1dd  9667  lediv1dd  9668  ltdiv23d  9670  lediv23d  9671  nn0ledivnn  9680  addlelt  9681  xrlelttr  9716  xrltletr  9717  xaddass2  9780  xltadd1  9786  xlt2add  9790  ixxdisj  9813  icoshftf1o  9901  icodisj  9902  lincmb01cmp  9913  iccf1o  9914  uzsubsubfz  9955  fzdisj  9960  fzopth  9969  fznatpl1  9984  fzsuc2  9987  fzp1disj  9988  fzrev2i  9994  uzdisj  10001  fseq1p1m1  10002  fzm1  10008  fzneuz  10009  fzp1nel  10012  fzrevral  10013  fznn0sub2  10036  fz0fzdiffz0  10038  difelfzle  10042  difelfznle  10043  nn0disj  10046  fzonnsub  10077  fzodisj  10086  fzouzdisj  10088  eluzgtdifelfzo  10105  ubmelfzo  10108  fzonn0p1p1  10121  ubmelm1fzo  10134  fzostep1  10145  exfzdc  10148  subfzo0  10150  qtri3or  10151  exbtwnzlemex  10158  rebtwn2z  10163  qbtwnrelemcalc  10164  qbtwnre  10165  qavgle  10167  apbtwnz  10182  flid  10192  flqwordi  10196  flqmulnn0  10207  flhalf  10210  flltdivnn0lt  10212  fldiv4p1lem1div2  10213  intfracq  10228  flqdiv  10229  flqpmodeq  10235  modqmulnn  10250  mulqaddmodid  10272  modqmuladdim  10275  modqmuladdnn0  10276  m1modge3gt1  10279  q2submod  10293  modaddmodup  10295  modqsubdir  10301  modqeqmodmin  10302  modfzo0difsn  10303  uzennn  10344  uzsinds  10350  monoord2  10385  ser3mono  10386  iseqf1olemqcl  10394  iseqf1olemnab  10396  iseqf1olemab  10397  iseqf1olemqf1o  10401  iseqf1olemqk  10402  seq3f1olemqsumkj  10406  seq3f1olemqsumk  10407  seq3f1olemqsum  10408  seq3f1olemp  10410  ser3le  10426  exp3val  10430  expnegap0  10436  expgt1  10466  ltexp2a  10480  le2sq2  10503  nnlesq  10531  bernneq  10547  expnbnd  10550  expnlbnd  10551  expnlbnd2  10552  expeq0d  10556  sq11d  10593  nn0ltexp2  10595  expcand  10602  nn0opthd  10607  facdiv  10623  faclbnd6  10629  facubnd  10630  facavg  10631  bcval4  10637  bcp1nk  10647  bcval5  10648  bcpasc  10651  hashennnuni  10664  focdmex  10672  isfinite4im  10678  hashnncl  10681  hashunlem  10689  fiprsshashgt1  10702  hashfzp1  10709  zfz1isolemiso  10721  seq3coll  10724  seq3shft  10749  cjth  10757  cjdivap  10820  cjne0d  10858  cjap0d  10859  cvg1nlemcxze  10893  cvg1nlemcau  10895  cvg1nlemres  10896  recvguniq  10906  resqrexlemover  10921  resqrexlemdecn  10923  resqrexlemlo  10924  resqrexlemcalc2  10926  resqrexlemcalc3  10927  resqrexlemnmsq  10928  resqrexlemnm  10929  resqrexlemcvg  10930  resqrexlemglsq  10933  resqrexlemga  10934  leabs  10985  absrele  10994  nn0abscl  10996  ltabs  10998  abslt  10999  absle  11000  abstri  11015  amgm2  11029  sqr11d  11084  abs00d  11097  maxabsle  11115  maxabslemlub  11118  maxleastlt  11126  maxltsup  11129  2zsupmax  11136  minmax  11140  xrmaxleim  11152  xrmaxiflemlub  11156  xrmaxiflemcom  11157  xrmaxiflemval  11158  xrmaxleastlt  11164  xrmaxltsup  11166  xrmaxaddlem  11168  xrmaxadd  11169  xrminmax  11173  xrmin1inf  11175  xrmin2inf  11176  xrmineqinf  11177  climi  11195  reccn2ap  11221  climge0  11233  climle  11242  climserle  11253  climrecvg1n  11256  fz1f1o  11283  summodclem3  11288  summodclem2a  11289  summodc  11291  fisumss  11300  fsum0diaglem  11348  mptfzshft  11350  fsumrev  11351  fisum0diag2  11355  fsumlessfi  11368  fsumle  11371  fsumlt  11372  isumsplit  11399  isumrpcl  11402  expcnvap0  11410  geosergap  11414  pwm1geoserap1  11416  absgtap  11418  geolim  11419  geolim2  11420  georeclim  11421  geoisumr  11426  geoisum1c  11428  cvgratnnlembern  11431  cvgratnnlemseq  11434  cvgratnnlemsumlt  11436  cvgratnnlemfm  11437  cvgratnnlemrate  11438  cvgratnn  11439  cvgratz  11440  mertenslemub  11442  mertenslemi1  11443  mertenslem2  11444  mertensabs  11445  prodmodclem2a  11484  prodmodc  11486  zproddc  11487  fprodntrivap  11492  fprodf1o  11496  fprodssdc  11498  fprodsplitdc  11504  fprodrev  11527  fprodmodd  11549  efcllemp  11566  ege2le3  11579  eftlcvg  11595  eftlub  11598  efltim  11606  eflegeo  11609  tanaddap  11647  sinbnd  11660  cosbnd  11661  sin01bnd  11665  cos01bnd  11666  sin01gt0  11669  cos01gt0  11670  cos12dec  11675  eirraplem  11684  zdvdsdc  11719  dvdstr  11735  dvdsadd2b  11746  dvdslelemd  11747  divconjdvds  11753  alzdvds  11758  dvdsext  11759  fzm1ndvds  11760  fzo0dvdseq  11761  zeo3  11771  even2n  11777  mod2eq1n2dvds  11782  nn0ehalf  11806  nnehalf  11807  nno  11809  nn0oddm1d2  11812  divalglemnqt  11823  divalglemex  11825  divalglemeuneg  11826  divalg2  11829  divalgmod  11830  flodddiv4t2lthalf  11840  zsupcllemstep  11844  infssuzex  11848  zsupssdc  11853  dvdsbnd  11855  gcdsupex  11856  gcdsupcl  11857  gcddvds  11862  divgcdz  11870  divgcdnn  11874  gcd0id  11878  gcdneg  11881  gcd1  11886  dvdsgcdidd  11893  bezoutlemnewy  11895  bezoutlemstep  11896  bezoutlemmo  11905  bezoutlemsup  11908  dfgcd3  11909  bezout  11910  dfgcd2  11913  mulgcd  11915  sqgcd  11928  dvdssqlem  11929  bezoutr1  11932  lcmval  11955  lcmcllem  11959  dvdslcm  11961  lcmgcdlem  11969  lcmdvds  11971  lcmgcdeq  11975  ncoprmgcdne1b  11981  mulgcddvds  11986  rpmulgcd2  11987  qredeu  11989  rpdvds  11991  prmind2  12012  nprm  12015  dvdsnprmd  12017  divgcdodd  12033  isprm6  12037  prmexpb  12041  pw2dvds  12056  pw2dvdseulemle  12057  oddpwdclemdc  12063  sqne2sq  12067  znege1  12068  sqrt2irraplemnn  12069  divnumden  12086  divdenle  12087  qden1elz  12095  nn0sqrtelqelz  12096  hashdvds  12111  crth  12114  phimullem  12115  eulerthlemfi  12118  eulerthlemh  12121  eulerthlemth  12122  eulerth  12123  prmdiv  12125  prmdiveq  12126  hashgcdlem  12128  phisum  12130  odzcllem  12132  odzdvds  12135  odzphi  12136  oddprm  12149  pythagtriplem3  12157  pythagtriplem4  12158  pythagtriplem10  12159  pythagtriplem11  12164  pythagtriplem13  12166  pythagtriplem19  12172  pcprendvds  12180  pcprendvds2  12181  pcpre1  12182  pcpremul  12183  pceulem  12184  pceu  12185  pczpre  12187  oddennn  12191  ennnfonelemk  12199  ennnfonelemkh  12211  ennnfonelemhf1o  12212  ennnfonelemex  12213  ennnfonelemhom  12214  ennnfonelemrnh  12215  ennnfonelemen  12220  ennnfonelemim  12223  ctinfomlemom  12226  ctiunctlemf  12237  ssnnctlemct  12245  nninfdclemcl  12249  nninfdclemp1  12251  nninfdclemlt  12252  unbendc  12255  ntridm  12596  ntrtop  12598  ntrcls0  12601  ntr0  12604  isopn3i  12605  neiss2  12612  opnneiss  12628  topssnei  12632  cnpf2  12677  icnpimaex  12681  lmcvg  12687  iscnp4  12688  cncnp  12700  cnptopresti  12708  lmfss  12714  lmtopcnp  12720  hmeores  12785  bldisj  12871  xblss2ps  12874  xblss2  12875  blhalf  12878  blssps  12897  blss  12898  ssblex  12901  blpnfctr  12909  xmetresbl  12910  mopni2  12953  bdxmet  12971  bdbl  12973  xmetxpbl  12978  metcnpi  12985  metcnpi2  12986  tgioo  13016  rescncf  13038  mulcncflem  13060  cnopnap  13064  dedekindeulemuub  13065  dedekindeulemloc  13067  dedekindeulemlu  13069  dedekindeu  13071  dedekindicclemuub  13074  dedekindicclemloc  13076  dedekindicclemlu  13078  dedekindicclemicc  13080  dedekindicc  13081  ivthinclemlopn  13084  ivthinclemuopn  13086  ivthdec  13092  limcimolemlt  13103  cnplimcim  13106  cnplimclemr  13108  limccnpcntop  13114  limccnp2cntop  13116  limccoap  13117  dvfgg  13127  dvidlemap  13130  dvaddxxbr  13135  dvmulxxbr  13136  dvaddxx  13137  dvmulxx  13138  dviaddf  13139  dvimulf  13140  dvcoapbr  13141  dvcjbr  13142  dvcj  13143  dvrecap  13147  dvmptclx  13150  dveflem  13157  reeff1oleme  13163  eflt  13166  sin0pilem1  13172  pilem3  13174  cosq14gt0  13223  coseq0negpitopi  13227  tangtx  13229  coskpi  13239  cosordlem  13240  cosq34lt1  13241  relogef  13255  logrpap0d  13269  rplogcl  13270  logge0  13271  logdivlti  13272  cxplt3  13310  rpabscxpbnd  13329  bj-charfunr  13456  pwf1oexmid  13642  subctctexmid  13644  pw1nct  13646  nnsf  13648  peano4nninf  13649  nninfsellemeq  13657  cvgcmp2nlemabs  13674  iooref1o  13676  trilpolemisumle  13680  trilpolemeq1  13682  trilpolemlt1  13683  trirec0  13686  apdifflemf  13688  apdifflemr  13689  apdiff  13690  iswomninnlem  13691  redcwlpo  13697  redc0  13699  reap0  13700  nconstwlpolemgt0  13705  neapmkvlem  13708  supfz  13710  inffz  13711