Theorem mpbid 195

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

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

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

This theorem is referenced by:  ax11eq 1362  ax11el 1363  eqtrd 1505  eleqtrd 1548  eueq2 1915  eueq3 1916  sbcth2 1979  csbexg 2005  csbeq2i 2017  sseqtrd 2094  3sstr3d 2100  elimdhyp 2392  breqtrd 2635  3brtr3d 2640  zfrepclf 2695  reuuniss 2885  reuuniss2 2887  reuhyp 2901  reuunixfr 2902  ordtri3or 2975  onint0 3003  onnmin 3011  onmindif2 3057  dflim3 3114  limsssuc 3117  finds 3152  tfindsg2 3159  fssres2 3639  feu 3642  f1orescnv 3699  fimacnv 3805  fopab2 3818  fopabco 3827  fsn2 3831  f1ocnvfv3 3878  tfrlem2 3907  oaass 4188  oelim2 4215  mapsn 4338  en2d 4390  mapenlem2 4479  xpmapenlem5 4489  phplem4 4500  php3 4504  php4 4505  unfilem1 4533  unifi 4541  fiint 4543  suppr 4573  supsnALT 4575  rankr1 4657  r1rankid 4677  rankr1id 4680  rankxplim 4695  rankxplim3 4697  aceq3 4716  cardnn 4807  cardaleph 4868  cardalephex 4869  axrepnd 4929  ltexprlem7 5131  cnegextlem3 5330  0cnALT 5333  nltpnftt 5549  ngtmnftt 5550  lediv12it 5854  recrecltt 5860  nn1suc 5897  nnleltp1t 5911  nnaddm1clt 5915  lbinfm 6005  infmrcl 6026  nnreclt 6029  nn0ltp1let 6084  elnnz1 6112  zaddclt 6122  zltp1let 6138  zextlet 6146  nn0ind-raph 6172  zmax 6178  zbtwnre 6179  rebtwnz 6180  flidt 6192  flval2t 6194  fladdzt 6199  flhalft 6201  ceim1lt 6204  seq1lem2 6260  seq1rn2 6271  ser1mono 6287  icoshftf1olem 6356  uznegit 6374  fznn0sub2t 6444  fzrev2it 6458  fzrev3it 6460  fzneuzt 6463  fzrevralt 6464  seqzrn2 6501  expordit 6545  exple1t 6552  le2sqit 6577  sqlecant 6586  bernneq 6597  expnbndt 6599  expnlbndt 6600  discrlem2 6602  discrlem3 6603  sqrlem12 6629  sqrlem13 6630  rimul 6690  crret 6717  crretOLD 6718  crimt 6719  crimtOLD 6720  absrelet 6819  absimlet 6820  facdivt 6894  facwordit 6896  faclbnd6 6906  facavgt 6907  bccl2t 6924  fsumrev 6982  fsumcmp 6993  fsumcmpndx2 6995  climrecl 7063  climge0 7065  climmullem4 7076  climcmplem 7090  clim2serz 7098  iserzex 7099  climserzle 7100  climubi 7106  caucvglem6 7115  ser1cmp 7127  ser1cmp2 7130  cvgcmp2lem 7133  infcvgaux2 7172  infcvglem1 7173  georeclim 7192  cvgratlem5 7206  fsum0diaglem1 7208  fsum0diag4 7213  ivthlem6 7238  ivthlem7 7239  ivthlem6OLD 7247  ivthlem7OLD 7248  erelem3 7280  efaddlem1 7297  efaddlem6 7302  efaddlem14 7310  efaddlem15 7311  efaddlem23 7319  ef1tllem 7340  ef01tllem2 7343  abspef01tlub 7353  efcnlem2 7377  efcn 7380  reeff1o 7385  subcost 7419  sinbndt 7424  cosbndt 7425  sin01bndlem2 7427  sin01bndlem3 7428  cos01bndlem2 7429  cos01bndlem3 7430  sin01gt0 7435  cos01gt0 7436  infpnlem2 7467  infxpidmlem10 7521  alephexp2 7546  opncld 7634  iincld 7639  clsidm 7658  ntridm 7659  clstop 7660  ntrtop 7661  ntrcls0 7667  cls0 7669  ntr0 7670  neiss2 7676  opnneiss 7692  metxp 7796  bl2in 7805  opni2 7827  lpbl 7842  methausi 7843  metcnpf 7845  metcnf 7846  lmnn 7897  lmuni 7913  bopcnlem3 7945  cmsss 7959  bcthlem16 7976  bcthlem18 7978  bcthlem19 7979  bcthlem21 7981  bcthlem24 7984  bcthlem33 7993  grp2inv 8040  vc0 8152  vcoprnelem 8161  vcoprne 8162  nvcni 8293  nvcni2 8294  nvcnpi4 8383  nmlno0lem 8413  nmblolbii 8418  ipasslem2 8450  ipasslem4 8452  ipasslem9 8457  minveclem9 8512  minveclem10 8513  minveclem14 8517  minveclem21 8524  minveclem24 8527  minveclem28 8531  htthlem10 8587  sinperlem1 8640  shftefif1olem 8696  eff1i 8699  his6t 8920  normpyct 8968  shorth 9123  projlem8 9148  projlem13 9153  projlem26 9166  pjthlem10 9183  pjthlem11 9184  choc1 9246  pjspansnt 9457  osumlem3 9537  5oalem3 9558  homulid2t 9683  homco1t 9684  homulasst 9685  hoadddit 9686  hoadddirt 9687  unopnormt 9798  unoplint 9801  elnlfn2t 9810  adjt 9814  adj2t 9815  adjadjt 9817  adjvalvalt 9818  hmoplint 9823  homco2t 9858  nmlnop0ALT 9876  nmopunt 9895  nmbdoplb 9905  nmcoplb 9914  nmophm 9917  lnopcon 9919  nmbdfnlb 9934  nmcfnlb 9943  lnfncon 9946  nlelch 9950  riesz3 9951  cnlnadjlem6 9961  adjlnopt 9975  nmopco 9984  cnvbravalt 9999  hmopidmch 10035  pjssdif1 10059  hstle1t 10109  hstlet 10113  hstoht 10115  stles 10124  stadd 10129  stadd3 10131  strlem1 10133  strlem3a 10135  strlem5 10138  dmdbr5 10191  mdsl2b 10206  chrelat 10247  atcvatlem 10268  irredlem4 10276  mdsymlem5 10290  sumdmdi 10298  cdj3lem2 10318  cdj3lem2b 10320  ghomfo 10347  cayleythlem 10369  ompfl3 10385  infi1 10405  mslb1 10545  2wsms 10546  msra3 10547  iintlem1 10548  trnij 10553

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