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 1540  eqsstrd 2085  3sstr4d 2094  eqbrtrd 2625  3brtr4d 2635  pwel 2749  opth1gOLD 2788  reuunixfr 2896  ordelon 2961  onin 2968  0ellim 3021  elelsuc 3031  onmindif 3050  onmindif2 3051  suceloni 3052  ordtri2or 3067  ssnlim 3157  relssdv 3239  iss 3381  funssres 3538  fn0 3591  fssxp 3622  fcoi1 3630  fcoi2 3631  fnopabfv 3743  fvco 3759  fvimacnvi 3789  fvimacnv 3790  fopabco 3817  fopabcos 3818  fsn 3819  fconst2g 3830  funfvima3 3839  f1ofveu 3867  tfrlem11 3906  tfrlem12 3907  tfr3 3911  tz7.48-2 3942  curry1 4082  curry1f 4083  oalim 4151  omlim 4152  oelim 4153  omlimcl 4193  oneo 4196  oen0 4197  enrefg 4371  pw2en 4426  mapenlem2 4470  mapxpen 4475  php 4493  onomeneq 4498  fodomfib 4541  iunfi 4543  supmo 4550  r1ord 4627  rankxplim3 4686  ac6lem 4726  fodomb 4772  oncard 4801  canth3 4822  ondomcard 4829  carduni 4830  alephfp 4872  cardcf 4883  cfeq0 4886  recrecpq 5045  ltaddpq 5051  genpn0 5078  ltsopr 5108  prlem934b 5110  ltaddpr 5112  reclem3pr 5130  1idsr 5179  ssgt0sr 5189  subdit 5399  ltpnft 5515  mnfltt 5516  pnfget 5521  mnflet 5522  xrlttrit 5525  xrlttrt 5526  xrret 5542  divdivdivt 5741  recp1lt1 5849  avglet 5991  lbinfm 5995  suprub 6003  suprleub 6006  xrsupsslem 6023  xrinfmsslem 6024  supxrre 6030  supxrub 6045  supxrleub 6046  nn0ge0t 6064  zltp1let 6128  zextlet 6136  gtndivt 6140  nn0ind-raph 6162  flleltt 6175  flidt 6180  flval3t 6182  fladdzt 6187  ceiget 6191  qbtwnxr 6217  qsqueeze 6218  ser1recl 6268  ndmioo 6307  iooid 6308  lbicc2t 6337  ubicc2t 6338  uzidt 6359  uznegit 6361  uz11t 6364  eluzp1lt 6366  elfzp1 6442  seqzeq 6487  expcllem 6507  expsubt 6529  exple1t 6538  discrlem3 6588  sqrlem12 6614  reim0t 6711  absdivz 6794  abssubne0t 6820  abs2dift 6839  abs2difabst 6840  faclbnd2 6883  faclbnd3 6884  faclbnd4lem3 6887  bccmplt 6900  bcnp11t 6903  bccl2t 6909  fsumsplit 6958  fsumrev 6967  ser1ser0 6986  climconst 7031  2climnn 7039  2climnn0 7040  climshft 7041  climrecl 7047  climge0 7049  climaddlem3 7052  climmullem8 7063  clim2serzt 7070  climcmplem 7073  clim2serz 7081  climsup 7091  serzf0 7105  ser1f0 7106  reccnv 7153  infcvglem1 7156  expcnv 7168  fsum0diaglem1 7191  fsum0diag4 7196  ivthlem7 7222  ivthlem7OLD 7231  efaddlem1 7280  efsubt 7313  eflegeolem1 7353  efcnlem1 7359  reeff1o 7368  cos2tt 7405  znnenlem 7443  znnen 7445  topbast 7569  subtop 7588  topcld 7617  0cld 7620  uncld 7623  elcls 7646  neif 7656  neiss 7664  elnei 7666  opnneissb 7669  ssnei2 7671  innei 7677  0nei 7680  qdensere 7691  idcn 7705  cnco 7707  cnpco 7708  iscncl 7709  cncnp 7717  cnconst 7719  sncld 7726  metsym 7755  metreslem 7762  blcntr 7785  blelrn 7788  opnm 7800  blnei 7818  tgioolem 7853  lmconst 7872  lmfexlem3 7893  lmle 7895  metelcls 7900  bopcnlem4 7918  iscms2lem3 7925  iscms2lem4 7926  cmsss 7931  cncms 7932  bcthlem9 7941  bcthlem22 7954  bcthlem26 7958  grpidinv2 7994  grpinv 8003  grpinvid 8009  grpinvf 8014  grpinvop 8015  grpdivf 8020  grplactf1o 8034  subgid 8057  invfval 8201  nvmf 8206  nvabs 8240  imsdf 8258  nvcnf 8265  nvcni 8266  va1cnlem 8279  sm1cnilem 8281  ipf 8300  sspid 8318  sspg 8321  ssps 8323  sspmlem 8325  sspn 8329  nvcnpi4 8355  nmblore 8378  0oo 8381  0lno 8382  0blo 8384  nmlno0lem 8385  ipasslem8 8428  ubthlem4 8463  ubthlem10 8469  minveclem9 8484  minveclem18 8493  minveclem29 8504  minveclem32 8507  minveclem36 8511  minveclem38 8513  hlcompl 8547  sinperlem2 8606  sincosq1eq 8626  efifolem7 8643  shftefif1olem 8661  shftefif1olemOLD 8662  hiidge0t 8885  hhcms 8993  ocsh 9072  occllem6 9094  projlem1 9102  projlem2 9103  projlem12 9113  projlem25 9126  projlem26 9127  omlsilem 9159  pjopt 9175  pjpot 9176  h1did 9389  cm0t 9469  osumlem3 9497  osumlem7 9501  5oalem1 9516  5oalem2 9517  3oalem2 9525  pjot 9533  hoaddclt 9601  homulclt 9602  nmopret 9714  hmopret 9763  brafnt 9787  kbopt 9793  kbpjt 9796  nmlnop0ALT 9835  nmophm 9876  nlelsh 9908  nlelch 9909  riesz3 9910  cnlnadjlem2 9916  cnlnadjlem5 9919  cnlnadjlem7 9921  nmopco 9942  nmopcoadj 9948  branmfnt 9951  leoprf2t 9972  leoprft 9973  leopsqt 9974  leopnmidt 9982  hmopidmchlem 9989  hmopidmch 9990  elpjrncht 10028  hstle1t 10063  hstlet 10067  sto2 10074  stle 10077  stles 10078  atord 10219  atcvat3 10231  atmd 10234  ghomgrpilem2 10291  ghomid 10299  ghomgsg 10300  ficli 10368  cdrci 10381  oisbmi 10384  oisbmj 10385  mapdiscn 10398  mapudiscn 10399  cmphmp 10408  idhme 10409  cnvhmpha 10412  hmphsyma 10415  hmphre 10417  hmeogrp 10425  homcard 10426  qusp 10430  fgsb 10444  infi 10448  fgsb2 10449  cnfilca 10451  clicls 10466  mslb1 10473  2wsms 10474  msra3 10475  iintlem1 10476  iint 10478  cnvtr 10482  aidm 10527  aidmold 10528  icmpmon 10587  idmon 10588

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