Theorem mpbird 196

Description: A deduction from a biconditional, related to modus ponens.

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 154	. 2 |- (ph -> (ch -> ps))
4	1, 3	mpd 26	1 |- (ph -> ps)

Syntax hints:   -> wi 3   <-> wb 146

This theorem is referenced by:  eqeltrd 1551  eqsstrd 2098  3sstr4d 2107  eqbrtrd 2640  3brtr4d 2650  pwel 2765  reuunixfr 2912  ordelon 2977  onin 2984  0ellim 3037  elelsuc 3047  onmindif 3066  onmindif2 3067  suceloni 3068  ordtri2or 3083  ssnlim 3173  relssdv 3255  iss 3403  funssres 3558  fn0 3611  fssxp 3643  fcoi1 3651  fcoi2 3652  fnopabfv 3764  fvco 3780  fvimacnvi 3810  fvimacnv 3811  fopabco 3838  fopabcos 3839  fsn 3840  fconst2g 3851  funfvima3 3860  f1ofveu 3888  tfrlem11 3927  tfrlem12 3928  tfr3 3932  tz7.48-2 3963  curry1 4104  curry1f 4105  oalim 4173  omlim 4174  oelim 4175  omlimcl 4215  oneo 4218  oen0 4219  enrefg 4396  pw2en 4452  mapenlem2 4496  mapxpen 4501  php 4519  onomeneq 4525  supmo 4585  supmax 4598  r1ord 4665  rankxplim3 4724  ac6lem 4764  fodomb 4810  oncard 4839  canth3 4861  ondomcard 4868  carduni 4869  alephfp 4911  cardcf 4923  cfeq0 4926  recrecpq 5085  ltaddpq 5091  genpn0 5118  ltsopr 5148  prlem934b 5150  ltaddpr 5152  reclem3pr 5170  1idsr 5219  ssgt0sr 5229  subdit 5439  ltpnft 5554  mnfltt 5555  pnfget 5560  mnflet 5561  xrlttrit 5564  xrlttrt 5565  xrret 5581  divdivdivt 5787  recp1lt1 5903  avglet 6046  lbinfm 6050  suprub 6058  suprleub 6061  xrsupsslem 6078  xrinfmsslem 6079  supxrre 6085  supxrub 6100  supxrleub 6101  nn0ge0t 6119  zltp1let 6183  zextlet 6191  gtndivt 6195  nn0ind-raph 6216  flleltt 6230  fraclt1t 6233  fracge0t 6234  flidt 6237  flval3t 6241  fladdzt 6246  ceiget 6250  quoremz 6253  intfracq 6255  fldivt 6256  qbtwnxr 6280  qsqueeze 6281  ser1recl 6332  ndmioo 6371  iooid 6372  lbicc2t 6405  ubicc2t 6406  uzidt 6428  uznegit 6430  uz11t 6433  eluzp1lt 6435  elfzp1 6511  seqzeq 6556  expcllem 6576  expsubt 6599  exple1t 6608  discrlem3 6659  sqrlem12 6685  reim0t 6775  absdivz 6859  abssubne0t 6882  abs2dift 6902  abs2difabst 6903  faclbnd2 6946  faclbnd3 6947  faclbnd4lem3 6950  bccmplt 6962  bcnp11t 6965  bccl2t 6971  fsumsplit 7020  fsumrev 7029  ser1ser0 7048  climconst 7094  2climnn 7102  2climnn0 7103  climshft 7104  climrecl 7110  climge0 7112  climaddlem3 7116  climmullem8 7127  clim2serzt 7134  climcmplem 7137  clim2serz 7145  climsup 7155  serzf0 7169  ser1f0 7170  reccnv 7218  infcvglem1 7221  expcnv 7233  cvgratlem5 7254  fsum0diaglem1 7256  fsum0diag4 7261  ivthlem7 7287  efaddlem1 7338  efsubt 7371  eflegeolem1 7413  efcnlem1 7419  reeff1o 7426  cos2tt 7463  cos2tsint 7464  znnenlem 7502  znnen 7503  topbast 7626  subtop 7643  topcld 7672  0cld 7675  uncld 7678  elcls 7701  neif 7712  neiss 7720  elnei 7722  opnneissb 7725  ssnei2 7727  innei 7733  0nei 7736  qdensere 7748  idcn 7763  cnco 7765  cnpco 7766  iscncl 7767  cncnp 7775  cnconst 7777  sncld 7784  metsym 7813  metreslem 7819  blcntr 7842  blelrn 7845  opnm 7857  blnei 7876  tgioolem 7911  lmconst 7931  lmfexlem3 7955  lmle 7957  metelcls 7962  bopcnlem4 7981  iscms2lem3 7988  iscms2lem4 7989  cmsss 7994  cncms 7995  bcthlem9 8004  bcthlem22 8017  bcthlem26 8021  grpidinv2 8056  grpinv 8065  grpinvid 8070  grpinvf 8075  grpinvop 8076  grpdivf 8081  grplactf1o 8094  subgid 8116  invfval 8257  nvmf 8262  nvabs 8297  imsdf 8316  nvcnf 8323  nvcnpf 8324  nvcni 8325  nvcni2 8326  va1cnlem 8341  sm1cnilem 8343  ipf 8362  sspid 8380  sspg 8383  ssps 8385  sspmlem 8387  sspn 8391  nvcnpi3 8418  nvcnpi4 8419  nmblore 8442  0oo 8445  0lno 8446  0blo 8448  nmlno0lem 8449  ipasslem8 8493  ubthlem4 8528  ubthlem10 8534  minveclem9 8549  minveclem18 8558  minveclem29 8569  minveclem32 8572  minveclem36 8576  minveclem38 8578  hlcompl 8613  pstr 8648  spwpr4OLD 8658  spwpr4aOLD 8659  sinperlem2 8682  sinkpi 8692  sincosq1eq 8704  sineq0 8708  efifolem7 8723  shftefif1olem 8736  hiidge0t 8959  hhcms 9067  ocsh 9151  occllem6 9173  projlem1 9181  projlem2 9182  projlem12 9192  projlem25 9205  projlem26 9206  omlsilem 9239  pjopt 9255  pjpot 9256  h1did 9469  cm0t 9547  osumlem3 9575  osumlem7 9579  5oalem1 9594  5oalem2 9595  3oalem2 9603  pjot 9611  hoaddclt 9679  homulclt 9680  nmopret 9792  hmopret 9842  brafnt 9866  kbopt 9872  kbpjt 9875  nmlnop0ALT 9915  nmophm 9956  nlelsh 9988  nlelch 9989  riesz3 9990  cnlnadjlem2 9996  cnlnadjlem5 9999  cnlnadjlem7 10001  nmopco 10023  nmopcoadj 10029  branmfnt 10033  bracnlnvalt 10042  leoprf2t 10055  leoprft 10056  leopsqt 10057  leopnmidt 10066  hmopidmchlem 10073  hmopidmch 10074  elpjrncht 10113  hstle1t 10148  hstlet 10152  sto2 10159  stle 10162  stles 10163  atord 10306  atcvat3 10318  atmd 10321  atdmd2 10336  ghomgrpilem2 10381  ghomid 10389  ghomgsg 10390  ficli 10462  inposet 10477  cdrci 10480  oisbmi 10483  oisbmj 10484  mapdiscn 10497  mapudiscn 10498  cmphmp 10507  idhme 10508  cnvhmpha 10511  hmphsyma 10514  hmphre 10516  hmeogrp 10524  homcard 10525  qusp 10541  fgsb 10555  infi 10559  fgsb2 10560  cnfilca 10562  rcfpfil 10569  clicls 10593  mslb1 10600  2wsms 10601  msra3 10602  iintlem1 10603  iint 10605  cnvtr 10609  aidm 10654  icmpmon 10715  idmon 10716  idfisf 10731

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147

Copyright terms: Public domain