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 1356  ax11el 1357  eqtrd 1499  eleqtrd 1542  eueq2 1909  eueq3 1910  sbcth2 1972  csbexg 1998  csbeq2i 2010  sseqtrd 2087  3sstr3d 2093  elimdhyp 2385  breqtrd 2629  3brtr3d 2634  zfrepclf 2689  opth1gOLD 2788  reuuniss 2879  reuuniss2 2881  reuhyp 2895  reuunixfr 2896  ordtri3or 2969  onint0 2997  onnmin 3005  onmindif2 3051  dflim3 3108  limsssuc 3111  finds 3146  tfindsg2 3153  fssres2 3629  feu 3632  f1orescnv 3689  fimacnv 3795  fopab2 3808  fopabco 3817  fsn2 3821  f1ocnvfv3 3868  tfrlem2 3897  oaass 4179  oelim2 4206  mapsn 4329  en2d 4381  mapenlem2 4470  xpmapenlem5 4480  phplem4 4491  php3 4495  php4 4496  unfilem1 4524  unifi 4532  fiint 4534  suppr 4562  supsnALT 4564  rankr1 4646  r1rankid 4666  rankr1id 4669  rankxplim 4684  rankxplim3 4686  aceq3 4705  cardnn 4796  cardaleph 4857  cardalephex 4858  axrepnd 4918  ltexprlem7 5120  cnegextlem3 5319  0cnALT 5322  nltpnftt 5539  ngtmnftt 5540  lediv12it 5844  recrecltt 5850  nn1suc 5887  nnleltp1t 5901  nnaddm1clt 5905  lbinfm 5995  infmrcl 6016  nnreclt 6019  nn0ltp1let 6074  elnnz1 6102  zaddclt 6112  zltp1let 6128  zextlet 6136  nn0ind-raph 6162  zmax 6168  zbtwnre 6169  rebtwnz 6170  flidt 6180  flval2t 6181  fladdzt 6187  flhalft 6189  ceim1lt 6192  seq1lem2 6247  seq1rn2 6258  ser1mono 6274  icoshftf1olem 6343  uznegit 6361  fznn0sub2t 6431  fzrev2it 6445  fzrev3it 6447  fzneuzt 6450  fzrevralt 6451  seqzrn2 6488  expordit 6531  exple1t 6538  le2sqit 6563  sqlecant 6572  bernneq 6583  expnbndt 6585  discrlem2 6587  discrlem3 6588  sqrlem12 6614  sqrlem13 6615  rimul 6675  crret 6702  crretOLD 6703  crimt 6704  crimtOLD 6705  absrelet 6804  absimlet 6805  facdivt 6879  facwordit 6881  faclbnd6 6891  facavgt 6892  bccl2t 6909  fsumrev 6967  fsumcmp 6978  fsumcmpndx2 6980  climrecl 7047  climge0 7049  climmullem4 7059  climcmplem 7073  clim2serz 7081  iserzex 7082  climserzle 7083  climubi 7089  caucvglem6 7098  ser1cmp 7110  ser1cmp2 7113  cvgcmp2lem 7116  infcvgaux2 7155  infcvglem1 7156  georeclim 7175  cvgratlem5 7189  fsum0diaglem1 7191  fsum0diag4 7196  ivthlem6 7221  ivthlem7 7222  ivthlem6OLD 7230  ivthlem7OLD 7231  erelem3 7263  efaddlem1 7280  efaddlem6 7285  efaddlem14 7293  efaddlem15 7294  efaddlem23 7302  ef1tllem 7323  ef01tllem2 7326  abspef01tlub 7336  efcnlem2 7360  efcn 7363  reeff1o 7368  subcost 7402  sinbndt 7407  cosbndt 7408  sin01bndlem2 7410  sin01bndlem3 7411  cos01bndlem2 7412  cos01bndlem3 7413  sin01gt0 7418  cos01gt0 7419  infpnlem2 7450  infxpidmlem10 7504  alephexp2 7528  opncld 7616  iincld 7621  clsidm 7640  ntridm 7641  clstop 7642  ntrtop 7643  ntrcls0 7649  cls0 7651  neiss2 7657  opnneiss 7673  metxp 7774  bl2in 7783  opni2 7805  lpbl 7819  methausi 7820  metcnpf 7822  metcnf 7823  lmnn 7873  lmuni 7886  bopcnlem3 7917  cmsss 7931  bcthlem16 7948  bcthlem18 7950  bcthlem19 7951  bcthlem21 7953  bcthlem24 7956  bcthlem33 7965  grp2inv 8013  vc0 8125  vcoprnelem 8135  vcoprne 8136  nvcni 8266  nvcnpi4 8355  nmlno0lem 8385  nmblolbii 8390  ipasslem2 8422  ipasslem4 8424  ipasslem9 8429  minveclem9 8484  minveclem10 8485  minveclem14 8489  minveclem21 8496  minveclem24 8499  minveclem28 8503  htthlem10 8559  sinperlem1 8605  shftefif1olem 8661  shftefif1olemOLD 8662  eff1i 8665  his6t 8886  normpyct 8934  shorth 9084  projlem8 9109  projlem13 9114  projlem26 9127  pjthlem10 9143  pjthlem11 9144  choc1 9206  pjspansnt 9417  osumlem3 9497  5oalem3 9518  homulid2t 9643  homco1t 9644  homulasst 9645  hoadddit 9646  hoadddirt 9647  unopnormt 9757  unoplint 9760  elnlfn2t 9769  adjt 9773  adj2t 9774  adjadjt 9776  adjvalvalt 9777  hmoplint 9782  homco2t 9817  nmlnop0ALT 9835  nmopunt 9854  nmbdoplb 9864  nmcoplb 9873  nmophm 9876  lnopcon 9878  nmbdfnlb 9893  nmcfnlb 9902  lnfncon 9905  nlelch 9909  riesz3 9910  cnlnadjlem6 9920  adjlnopt 9934  nmopco 9942  cnvbravalt 9956  hmopidmch 9990  pjssdif1 10014  hstle1t 10063  hstlet 10067  hstoht 10069  stles 10078  stadd 10083  stadd3 10085  strlem1 10087  strlem3a 10089  strlem5 10092  mdsl2b 10158  chrelat 10199  atcvatlem 10220  irredlem4 10228  mdsymlem5 10242  sumdmdi 10249  cdj3lem2 10267  cdj3lem2b 10269  ghomfo 10296  cayleythlem 10320  infi1 10347  mslb1 10473  2wsms 10474  msra3 10475  iintlem1 10476  trnij 10481

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