Theorem mpbird 167

Description: A deduction from a biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
mpbird.min	|- ( ph -> ch )
mpbird.maj	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
mpbird	|- ( ph -> ps )

Proof of Theorem mpbird

Step	Hyp	Ref	Expression
1		mpbird.min	. 2 |- ( ph -> ch )
2		mpbird.maj	. . 3 |- ( ph -> ( ps <-> ch ) )
3	2	biimprd 158	. 2 |- ( ph -> ( ch -> ps ) )
4	1, 3	mpd 13	1 |- ( ph -> ps )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpbiri  168  pm5.19  706  mpbir2and  944  pm3.12dc  958  mpbir3and  1180  pm5.15dc  1389  eqeltrd  2254  eqnetrd  2371  3netr4d  2380  r19.30dc  2624  sbcne12g  3076  eqsstrd  3192  3sstr4d  3201  eqbrtrd  4026  3brtr4d  4036  snelpwi  4213  prelpwi  4215  pwel  4219  ordelon  4384  onin  4387  elelsuc  4410  onsuc  4501  onsucb  4503  onintonm  4517  omsinds  4622  sosng  4700  relssdv  4719  eqbrrdv  4724  eqrelrdv2  4726  relsnopg  4731  breldmg  4834  elrnmptdv  4882  iss  4954  xpimasn  5078  elxp4  5117  elxp5  5118  iotam  5209  funssres  5259  f0rn0  5411  sefvex  5537  fvun1  5583  eqfnfvd  5617  fvimacnvi  5631  fvimacnv  5632  fvelrn  5648  fmpt3d  5673  fmpt2d  5679  resflem  5681  fmptco  5683  fsn  5689  ftpg  5701  fconst2g  5732  funfvima3  5751  foeqcnvco  5791  f1eqcocnv  5792  fliftfun  5797  fliftfund  5798  fliftval  5801  riota5f  5855  f1ofveu  5863  f1ocnvd  6073  f1opw2  6077  off  6095  offval2  6098  ofrfval2  6099  caofref  6104  caofinvl  6105  elxp6  6170  cnvf1olem  6225  f2ndf  6227  f1od2  6236  tposf12  6270  smores2  6295  tfrlemisucaccv  6326  tfrlemibfn  6329  tfr1onlemsucaccv  6342  tfr1onlembfn  6345  tfrcllemsucaccv  6355  tfrcllembfn  6358  tfrcl  6365  tfri3  6368  frecabcl  6400  nnsucsssuc  6493  ersym  6547  ertr  6550  swoer  6563  erth  6579  riinerm  6608  qliftfund  6618  eroprf  6628  ecopoverg  6636  th3qlem1  6637  elmapssres  6673  mapss  6691  fdiagfn  6692  ixpssmap2g  6727  mapsnf1o  6737  f1dom2g  6756  dom3d  6774  fopwdom  6836  mapxpen  6848  nndomo  6864  dif1en  6879  findcard2  6889  findcard2s  6890  diffisn  6893  fimax2gtrilemstep  6900  fientri3  6914  fiintim  6928  f1dmvrnfibi  6943  sbthlemi6  6961  elfir  6972  fifo  6979  supelti  7001  supsnti  7004  cnvinfex  7017  ordiso2  7034  updjud  7081  djudom  7092  difinfsn  7099  ctssdc  7112  enumctlemm  7113  enumct  7114  enomnilem  7136  fodjuf  7143  ismkvnex  7153  omnimkv  7154  enmkvlem  7159  enwomnilem  7167  nninfdcinf  7169  nninfwlporlem  7171  isnumi  7181  exmidfodomrlemrALT  7202  djudoml  7218  djudomr  7219  netap  7253  2omotaplemap  7256  2omotaplemst  7257  exmidapne  7259  cc2lem  7265  cc3  7267  ltsopi  7319  pitri3or  7321  ltdcpi  7322  indpi  7341  enqdc  7360  enqdc1  7361  addcmpblnq  7366  mulcanenq  7384  recrecnq  7393  nqtri3or  7395  ltdcnq  7396  ltsonq  7397  ltaddnq  7406  subhalfnqq  7413  archnqq  7416  prarloclemarch2  7418  enq0tr  7433  nqnq0  7440  addcmpblnq0  7442  mulcanenq0ec  7444  nnnq0lem1  7445  nqpnq0nq  7452  nq0m0r  7455  nq02m  7464  prarloclemlt  7492  prarloclemcalc  7501  addlocpr  7535  nqprl  7550  nqpru  7551  addnqprlemrl  7556  addnqprlemru  7557  prmuloclemcalc  7564  mullocprlem  7569  mulnqprlemrl  7572  mulnqprlemru  7573  1idprl  7589  1idpru  7590  ltaddpr  7596  ltexprlemm  7599  ltexprlemopl  7600  ltexprlemopu  7602  ltexprlemdisj  7605  ltexprlemrl  7609  ltexprlemru  7611  addcanprleml  7613  addcanprlemu  7614  addcanprg  7615  prplnqu  7619  recexprlemloc  7630  recexprlem1ssl  7632  recexprlem1ssu  7633  aptiprleml  7638  aptiprlemu  7639  archpr  7642  cauappcvgprlemm  7644  cauappcvgprlemopl  7645  cauappcvgprlemloc  7651  cauappcvgprlemladdfu  7653  cauappcvgprlemladdfl  7654  cauappcvgprlem1  7658  cauappcvgprlem2  7659  caucvgprlemnkj  7665  caucvgprlemopl  7668  caucvgprlemloc  7674  caucvgprlemladdfu  7676  caucvgprlem2  7679  caucvgprprlemnkltj  7688  caucvgprprlemopl  7696  caucvgprprlemloc  7702  caucvgprprlemexbt  7705  caucvgprprlemaddq  7707  caucvgprprlem2  7709  suplocexprlemmu  7717  suplocexprlemru  7718  suplocexprlemloc  7720  suplocexprlemlub  7723  prsrlem1  7741  0idsr  7766  1idsr  7767  recexgt0sr  7772  archsr  7781  prsradd  7785  caucvgsrlemcau  7792  caucvgsrlembound  7793  caucvgsrlemoffgt1  7798  suplocsrlemb  7805  suplocsrlempr  7806  suplocsrlem  7807  pitonnlem1p1  7845  pitonn  7847  pitoregt0  7848  peano2nnnn  7852  recidpirq  7857  axcaucvglemval  7896  leid  8041  nltled  8078  readdcan  8097  addneintrd  8145  addneintr2d  8146  pncan  8163  subsub2  8185  subsub4  8190  negned  8265  subne0d  8277  subneintrd  8312  subneintr2d  8314  subeq0bd  8336  subdi  8342  gt0add  8530  rimul  8542  rereim  8543  ltmul1a  8548  apreim  8560  apirr  8562  mulap0r  8572  msqge0  8573  mulge0  8576  gt0ap0  8583  ltap  8590  subap0d  8601  recexaplem2  8609  mulap0bad  8616  mulap0bbd  8617  mul0eqap  8627  divrecap  8645  div0ap  8659  div1  8660  recrecap  8666  divdivdivap  8670  ddcanap  8683  rerecclap  8687  div2negap  8692  diveqap1bd  8793  recgt0  8807  prodgt0  8809  lemul1a  8815  recp1lt1  8856  squeeze0  8861  peano2nn  8931  div4p1lem1div2  9172  arch  9173  peano2z  9289  peano2zm  9291  ztri3or  9296  nn0n0n1ge2  9323  zextle  9344  gtndiv  9348  suprzclex  9351  nn0ind-raph  9370  uzid  9542  uzneg  9546  uztric  9549  uz11  9550  eluzp1l  9552  qdivcl  9643  irrmul  9647  rpnegap  9686  negelrpd  9688  ledivge1le  9726  mul2lt0rlt0  9759  mul2lt0rgt0  9760  nn0ledivnn  9767  ltpnf  9780  mnflt  9783  pnfge  9789  mnfle  9792  xrlttr  9795  xrltso  9796  xrlttri3  9797  xrleid  9800  xaddass2  9870  xltadd1  9876  xlt2add  9880  xleaddadd  9887  iccf1o  10004  fztri3or  10039  fznlem  10041  fzn  10042  fzsplit2  10050  fznatpl1  10076  uzsplit  10092  fseq1p1m1  10094  fzm1  10100  fznn0sub2  10128  difelfznle  10135  1fv  10139  fzodcel  10152  fzospliti  10176  fzouzsplit  10179  eluzgtdifelfzo  10197  exfzdc  10240  subfzo0  10242  exbtwnz  10251  qbtwnrelemcalc  10256  flqlelt  10276  qfraclt1  10280  qfracge0  10281  flqltnz  10287  btwnzge0  10300  flhalf  10302  ceiqle  10313  intfracq  10320  mulqmod0  10330  modqge0  10332  modqlt  10333  modqid  10349  modqid0  10350  m1modge3gt1  10371  modqltm1p1mod  10376  q2txmodxeq0  10384  modaddmodlo  10388  modsumfzodifsn  10396  addmodlteq  10398  frecuzrdgtcl  10412  frecuzrdgtclt  10421  uzennn  10436  uzsinds  10442  seqf  10461  seqf2  10464  monoord2  10477  iseqf1olemqk  10494  iseqf1olemjpcl  10495  iseqf1olemqpcl  10496  seq3f1olemqsumkj  10498  seq3f1olemqsum  10500  seq3f1olemstep  10501  seq3f1oleml  10503  ser3le  10518  exp3vallem  10521  exp3val  10522  expp1  10527  expcllem  10531  ltexp2a  10572  leexp2a  10573  nn0ltexp2  10689  faclbnd  10721  faclbnd2  10722  faclbnd3  10723  bcval5  10743  bcpasc  10746  hashennn  10760  fihasheqf1oi  10767  hashsng  10778  fihashfn  10780  hashun  10785  fihashss  10796  fihashssdif  10798  hashfz  10801  hashxp  10806  fimaxq  10807  zfz1isolem1  10820  seq3coll  10822  shftfn  10833  cjth  10855  cjmulrcl  10896  reim0bd  10953  rerebd  10954  cjrebd  10955  caucvgre  10990  cvg1nlemcxze  10991  cvg1nlemcau  10993  cvg1nlemres  10994  recvguniq  11004  resqrexlemover  11019  resqrexlemdec  11020  resqrexlemgt0  11029  resqrexlemoverl  11030  resqrexlemglsq  11031  rersqrtthlem  11039  sqrtgt0  11043  leabs  11083  absexpzap  11089  absle  11098  recvalap  11106  abstri  11113  abs2dif  11115  amgm2  11127  absne0d  11196  maxleim  11214  maxabslemab  11215  maxabslemlub  11216  maxltsup  11227  zmaxcl  11233  fimaxre2  11235  minmax  11238  rpmincl  11246  bdtrilem  11247  bdtri  11248  xrmaxleim  11252  xrmaxiflemcom  11257  xrmaxltsup  11266  xrmaxadd  11269  xrminmax  11273  xrminrpcl  11282  climconst  11298  climuni  11301  2clim  11309  climcn1  11316  climcn2  11317  reccn2ap  11321  climge0  11333  climle  11342  climsqz  11343  climsqz2  11344  serf0  11360  summodclem3  11388  summodclem2a  11389  fsumcl2lem  11406  sumpr  11421  sumtp  11422  fsum0diaglem  11448  mptfzshft  11450  fsumle  11471  fsumlt  11472  divcnv  11505  trireciplem  11508  expcnvap0  11510  expcnv  11512  explecnv  11513  geosergap  11514  cvgratnnlembern  11531  cvgratnnlemabsle  11535  cvgratnnlemsumlt  11536  cvgratz  11540  cvgratgt0  11541  mertenslemi1  11543  mertenslem2  11544  mertensabs  11545  clim2divap  11548  prodmodclem3  11583  prodmodclem2a  11584  fprodseq  11591  fprodmul  11599  fprodfac  11623  fprodconst  11628  fprodap0  11629  fprodap0f  11644  fprodle  11648  eftcl  11662  ef0lem  11668  efsub  11689  eftlub  11698  eflegeo  11709  tanval2ap  11721  sinadd  11744  cos2t  11758  cos2tsin  11759  sin01bnd  11765  cos01bnd  11766  eirraplem  11784  dvdsval2  11797  dvdsdc  11805  dvds0lem  11808  zdvdsdc  11819  dvdscmulr  11827  dvdsmulcr  11828  dvdslelemd  11849  divconjdvds  11855  dvdsext  11861  fzm1ndvds  11862  dvdsmod  11868  oexpneg  11882  2tp1odd  11889  mulsucdiv2z  11890  2teven  11892  zeo5  11893  opeo  11902  omeo  11903  nn0ob  11913  divalglemnqt  11925  zsupcllemstep  11946  zsupcl  11948  zssinfcl  11949  infssuzex  11950  infssuzcldc  11952  suprzubdc  11953  nninfdcex  11954  gcddvds  11964  dvdslegcd  11965  gcdneg  11983  bezoutlemnewy  11997  bezoutlemstep  11998  bezoutlema  12000  bezoutlemb  12001  bezoutlemmo  12007  bezoutlemle  12009  bezoutlemsup  12010  dfgcd3  12011  bezout  12012  dfgcd2  12015  uzwodc  12038  lcmcllem  12067  lcmneg  12074  lcmgcdlem  12077  lcmdvds  12079  lcmid  12080  3lcm2e6woprm  12086  6lcm4e12  12087  ncoprmgcdne1b  12089  mulgcddvds  12094  divgcdcoprmex  12102  cncongr1  12103  cncongr2  12104  isprm2lem  12116  prmind2  12120  dvdsnprmd  12125  prm2orodd  12126  sqnprm  12136  isprm5lem  12141  rpexp  12153  sqrt2irrlem  12161  oddpwdclemdc  12173  sqrt2irraplemnn  12179  qnumdencoprm  12193  qeqnumdivden  12194  nn0gcdsq  12200  nn0sqrtelqelz  12206  nonsq  12207  phicl2  12214  phibnd  12217  hashdvds  12221  phiprmpw  12222  phimullem  12225  eulerthlemrprm  12229  eulerthlema  12230  eulerthlemth  12232  prmdiveq  12236  hashgcdlem  12238  odzdvds  12245  modprminv  12249  nnnn0modprm0  12255  modprmn0modprm0  12256  pythagtriplem10  12269  pythagtriplem19  12282  pythagtrip  12283  pcpre1  12292  pcpremul  12293  pceu  12295  pcmul  12301  pcdiv  12302  pcqmul  12303  pcqdiv  12307  pcexp  12309  pcdvdsb  12319  pcidlem  12322  pcdvdstr  12326  pcgcd1  12327  pc2dvds  12329  pcprmpw2  12332  difsqpwdvds  12337  pcaddlem  12338  pcadd  12339  pcmpt  12341  pcmptdvds  12343  pcprod  12344  fldivp1  12346  pcfaclem  12347  pcfac  12348  pcbc  12349  qexpz  12350  pockthlem  12354  pockthg  12355  1arithlem4  12364  1arith  12365  1arith2  12366  4sqlem6  12381  4sqlem8  12383  4sqlem9  12384  4sqlem10  12385  znnen  12399  ennnfonelemk  12401  ennnfonelemkh  12413  ennnfonelemhf1o  12414  ennnfonelemrnh  12417  ennnfonelemfun  12418  ennnfonelemf1  12419  ennnfonelemrn  12420  ennnfonelemnn0  12423  ctinfomlemom  12428  ctiunctlemudc  12438  unct  12443  omctfn  12444  ssnnctlemct  12447  nninfdclemp1  12451  nninfdc  12454  structfung  12479  setsfun  12497  setsfun0  12498  setscom  12502  setsslid  12513  imasaddfnlemg  12735  imasaddvallemg  12736  mgmsscl  12780  plusffng  12784  mgmplusf  12785  mgm0  12788  mgm1  12789  opifismgmdc  12790  sgrp1  12816  mndpfo  12839  mndfo  12840  mnd1  12847  0subm  12871  mhmima  12875  grpinvfng  12917  isgrpinv  12926  grpinvid  12930  grpinvf1o  12940  grpinvadd  12948  grpsubf  12949  grpsubsub4  12963  grplactcnv  12972  grp1  12976  grp1inv  12977  mulgfng  12987  subginv  13041  resgrpisgrp  13055  subgintm  13058  0subg  13059  0nsg  13074  srgideu  13155  srgidmlem  13161  srgpcomp  13173  srg1expzeq1  13178  ringcl  13196  ringideu  13200  ringidmlem  13205  ringnegl  13228  ringnegr  13229  ring1  13236  opprringbg  13250  dvdsrd  13263  dvdsr01  13273  isunitd  13275  unitinvcl  13292  unitinvinv  13293  unitnegcl  13299  nzrunit  13329  lringuplu  13337  subrgsubm  13355  subrgintm  13364  aprsym  13374  scaffng  13399  lmodscaf  13400  cnfldneg  13470  zringinvg  13497  baspartn  13553  eltg3i  13559  tgclb  13568  topbas  13570  2basgeng  13585  topcld  13612  0cld  13615  uncld  13616  neif  13644  elnei  13655  0nei  13669  restbasg  13671  iscnp4  13721  cnpnei  13722  cnclima  13726  cncnp  13733  cnrest2r  13740  cndis  13744  lmff  13752  lmtopcnp  13753  txbas  13761  txopn  13768  txcnp  13774  upxp  13775  txdis1cn  13781  cnmpt11  13786  cnmpt21  13794  psmetge0  13834  xmetge0  13868  xmettpos  13873  xmetrtri  13879  metrtri  13880  xblpnfps  13901  xblpnf  13902  blfps  13912  blf  13913  ssblps  13928  ssbl  13929  blbas  13936  metss2  14001  xmettxlem  14012  xmettx  14013  qtopbas  14025  divcnap  14058  cncfss  14073  cdivcncfap  14090  expcncf  14095  cnopnap  14097  dedekindeulemuub  14098  dedekindeulemlu  14102  dedekindeu  14104  suplociccex  14106  dedekindicclemuub  14107  dedekindicclemlu  14111  dedekindicclemicc  14113  ivthinclemlopn  14117  ivthinclemuopn  14119  ivthinc  14124  ellimc3apf  14132  limcimolemlt  14136  limcimo  14137  limcresi  14138  cnplimclemle  14140  reldvg  14151  dvfgg  14160  dvidlemap  14163  dvcjbr  14175  dvcj  14176  dvrecap  14180  dveflem  14190  dvef  14191  reeff1oleme  14196  pilem3  14207  sinq34lt0t  14255  cosq14gt0  14256  coseq0q4123  14258  tangtx  14262  sincosq1eq  14263  cosordlem  14273  logdivlti  14305  relogbval  14372  relogbzcl  14373  nnlogbexp  14380  logbgcd1irr  14388  logbgcd1irraplemexp  14389  logbgcd1irraplemap  14390  zabsle1  14403  lgslem1  14404  lgsval  14408  lgsfvalg  14409  lgsfcl2  14410  lgsval2lem  14414  lgscl1  14427  lgsmod  14430  lgsdir2lem5  14436  lgsdir2  14437  lgsdilem2  14440  lgsdi  14441  lgsne0  14442  lgseisenlem1  14453  lgseisenlem2  14454  2lgsoddprmlem2  14457  2sqlem3  14467  2sqlem8  14473  2sqlem10  14475  fnmptd  14559  bj-sels  14669  bj-nnelon  14714  pwle2  14751  pwf1oexmid  14752  pw1nct  14755  nninfall  14761  nninfsellemdc  14762  nninfself  14765  refeq  14779  isomninnlem  14781  cvgcmp2nlemabs  14783  trilpolemlt1  14792  trirec0  14795  apdifflemf  14797  apdifflemr  14798  apdiff  14799  iswomninnlem  14800  iswomni0  14802  ismkvnnlem  14803  reap0  14809