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 1545  eqsstrd 2091  3sstr4d 2100  eqbrtrd 2630  3brtr4d 2640  pwel 2754  reuunixfr 2901  ordelon 2966  onin 2973  0ellim 3026  elelsuc 3036  onmindif 3055  onmindif2 3056  suceloni 3057  ordtri2or 3072  ssnlim 3162  relssdv 3244  iss 3389  funssres 3544  fn0 3597  fssxp 3628  fcoi1 3636  fcoi2 3637  fnopabfv 3749  fvco 3765  fvimacnvi 3795  fvimacnv 3796  fopabco 3823  fopabcos 3824  fsn 3825  fconst2g 3836  funfvima3 3845  f1ofveu 3873  tfrlem11 3912  tfrlem12 3913  tfr3 3917  tz7.48-2 3948  curry1 4088  curry1f 4089  oalim 4157  omlim 4158  oelim 4159  omlimcl 4199  oneo 4202  oen0 4203  enrefg 4377  pw2en 4432  mapenlem2 4476  mapxpen 4481  php 4499  onomeneq 4504  fodomfib 4547  iunfi 4549  supmo 4556  supmax 4569  r1ord 4635  rankxplim3 4694  ac6lem 4734  fodomb 4780  oncard 4809  canth3 4830  ondomcard 4837  carduni 4838  alephfp 4880  cardcf 4891  cfeq0 4894  recrecpq 5053  ltaddpq 5059  genpn0 5086  ltsopr 5116  prlem934b 5118  ltaddpr 5120  reclem3pr 5138  1idsr 5187  ssgt0sr 5197  subdit 5407  ltpnft 5523  mnfltt 5524  pnfget 5529  mnflet 5530  xrlttrit 5533  xrlttrt 5534  xrret 5550  divdivdivt 5749  recp1lt1 5857  avglet 5999  lbinfm 6003  suprub 6011  suprleub 6014  xrsupsslem 6031  xrinfmsslem 6032  supxrre 6038  supxrub 6053  supxrleub 6054  nn0ge0t 6072  zltp1let 6136  zextlet 6144  gtndivt 6148  nn0ind-raph 6170  flleltt 6183  flidt 6188  flval3t 6190  fladdzt 6195  ceiget 6199  qbtwnxr 6225  qsqueeze 6226  ser1recl 6276  ndmioo 6315  iooid 6316  lbicc2t 6345  ubicc2t 6346  uzidt 6367  uznegit 6369  uz11t 6372  eluzp1lt 6374  elfzp1 6450  seqzeq 6495  expcllem 6515  expsubt 6537  exple1t 6546  discrlem3 6596  sqrlem12 6622  reim0t 6719  absdivz 6802  abssubne0t 6828  abs2dift 6847  abs2difabst 6848  faclbnd2 6891  faclbnd3 6892  faclbnd4lem3 6895  bccmplt 6908  bcnp11t 6911  bccl2t 6917  fsumsplit 6966  fsumrev 6975  ser1ser0 6994  climconst 7039  2climnn 7047  2climnn0 7048  climshft 7049  climrecl 7055  climge0 7057  climaddlem3 7060  climmullem8 7071  clim2serzt 7078  climcmplem 7081  clim2serz 7089  climsup 7099  serzf0 7113  ser1f0 7114  reccnv 7161  infcvglem1 7164  expcnv 7176  fsum0diaglem1 7199  fsum0diag4 7204  ivthlem7 7230  ivthlem7OLD 7239  efaddlem1 7288  efsubt 7321  eflegeolem1 7361  efcnlem1 7367  reeff1o 7376  cos2tt 7413  znnenlem 7451  znnen 7453  topbast 7577  subtop 7596  topcld 7625  0cld 7628  uncld 7631  elcls 7654  neif 7665  neiss 7673  elnei 7675  opnneissb 7678  ssnei2 7680  innei 7686  0nei 7689  qdensere 7701  idcn 7716  cnco 7718  cnpco 7719  iscncl 7720  cncnp 7728  cnconst 7730  sncld 7737  metsym 7766  metreslem 7774  blcntr 7797  blelrn 7800  opnm 7812  blnei 7831  tgioolem 7866  lmconst 7886  lmfexlem3 7909  lmle 7911  metelcls 7916  bopcnlem4 7934  iscms2lem3 7941  iscms2lem4 7942  cmsss 7947  cncms 7948  bcthlem9 7957  bcthlem22 7970  bcthlem26 7974  grpidinv2 8010  grpinv 8019  grpinvid 8024  grpinvf 8029  grpinvop 8030  grpdivf 8035  grplactf1o 8049  subgid 8072  invfval 8213  nvmf 8218  nvabs 8253  imsdf 8271  nvcnf 8278  nvcni 8279  va1cnlem 8292  sm1cnilem 8294  ipf 8313  sspid 8331  sspg 8334  ssps 8336  sspmlem 8338  sspn 8342  nvcnpi4 8368  nmblore 8391  0oo 8394  0lno 8395  0blo 8397  nmlno0lem 8398  ipasslem8 8441  ubthlem4 8476  ubthlem10 8482  minveclem9 8497  minveclem18 8506  minveclem29 8517  minveclem32 8520  minveclem36 8524  minveclem38 8526  hlcompl 8560  pstr 8594  sinperlem2 8625  sincosq1eq 8645  efifolem7 8662  shftefif1olem 8680  hiidge0t 8903  hhcms 9011  ocsh 9095  occllem6 9117  projlem1 9125  projlem2 9126  projlem12 9136  projlem25 9149  projlem26 9150  omlsilem 9182  pjopt 9198  pjpot 9199  h1did 9412  cm0t 9492  osumlem3 9520  osumlem7 9524  5oalem1 9539  5oalem2 9540  3oalem2 9548  pjot 9556  hoaddclt 9624  homulclt 9625  nmopret 9737  hmopret 9786  brafnt 9810  kbopt 9816  kbpjt 9819  nmlnop0ALT 9858  nmophm 9899  nlelsh 9931  nlelch 9932  riesz3 9933  cnlnadjlem2 9939  cnlnadjlem5 9942  cnlnadjlem7 9944  nmopco 9966  nmopcoadj 9972  branmfnt 9976  bracnlnvalt 9985  leoprf2t 9998  leoprft 9999  leopsqt 10000  leopnmidt 10009  hmopidmchlem 10016  hmopidmch 10017  elpjrncht 10056  hstle1t 10091  hstlet 10095  sto2 10102  stle 10105  stles 10106  atord 10248  atcvat3 10260  atmd 10263  ghomgrpilem2 10320  ghomid 10328  ghomgsg 10329  gelsupvalOLD 10354  ficli 10404  cdrci 10417  oisbmi 10420  oisbmj 10421  mapdiscn 10434  mapudiscn 10435  cmphmp 10444  idhme 10445  cnvhmpha 10448  hmphsyma 10451  hmphre 10453  hmeogrp 10461  homcard 10462  qusp 10466  fgsb 10480  infi 10484  fgsb2 10485  cnfilca 10487  clicls 10502  mslb1 10509  2wsms 10510  msra3 10511  iintlem1 10512  iint 10514  cnvtr 10518  aidm 10563  aidmold 10564  icmpmon 10623  idmon 10624

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