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 1363  ax11el 1364  eqtrd 1507  eleqtrd 1550  eueq2 1918  eueq3 1919  sbcth2 1982  csbexg 2008  csbeq2i 2020  sseqtrd 2097  3sstr3d 2103  elimdhyp 2395  breqtrd 2639  3brtr3d 2644  zfrepclf 2699  reuuniss 2889  reuuniss2 2891  reuhyp 2905  reuunixfr 2906  ordtri3or 2979  onint0 3007  onnmin 3015  onmindif2 3061  dflim3 3118  limsssuc 3121  finds 3156  tfindsg2 3163  fssres2 3644  feu 3647  f1orescnv 3704  fimacnv 3810  fopab2 3823  fopabco 3832  fsn2 3836  f1ocnvfv3 3883  tfrlem2 3912  oaass 4195  oelim2 4222  mapsn 4345  en2d 4399  mapenlem2 4488  xpmapenlem5 4498  phplem4 4509  php3 4513  php4 4514  unfilem1 4543  unifi 4550  fiint 4552  suppr 4582  supsnALT 4584  rankr1 4666  r1rankid 4686  rankr1id 4689  rankxplim 4704  rankxplim3 4706  aceq3 4725  cardnn 4816  cardaleph 4877  cardalephex 4878  axrepnd 4938  ltexprlem7 5140  cnegextlem3 5339  0cnALT 5342  nltpnftt 5558  ngtmnftt 5559  lediv12it 5884  recrecltt 5890  nn1suc 5927  nnleltp1t 5942  nnaddm1clt 5946  lbinfm 6036  infmrcl 6057  nnreclt 6060  nn0ltp1let 6115  elnnz1 6143  zaddclt 6153  zltp1let 6169  zextlet 6177  nn0ind-raph 6202  zmax 6208  zbtwnre 6209  rebtwnz 6210  flidt 6223  flval2t 6225  fladdzt 6231  flhalft 6233  ceim1lt 6236  intfracq 6241  seq1lem2 6296  seq1rn2 6307  ser1mono 6323  icoshftf1olem 6396  uznegit 6415  fznn0sub2t 6485  fzrev2it 6499  fzrev3it 6501  fzneuzt 6504  fzrevralt 6505  seqzrn2 6542  expordit 6586  exple1t 6593  le2sqit 6618  sqlecant 6627  bernneq 6638  expnbndt 6640  expnlbndt 6641  discrlem2 6643  discrlem3 6644  sqrlem12 6670  sqrlem13 6671  rimul 6730  crret 6755  crimt 6756  absrelet 6854  absimlet 6855  facdivt 6927  facwordit 6929  faclbnd6 6939  facavgt 6940  bccl2t 6956  fsumrev 7014  fsumcmp 7025  fsumcmpndx2 7027  climrecl 7095  climge0 7097  climmullem4 7108  climcmplem 7122  clim2serz 7130  iserzex 7131  climserzle 7132  climubi 7138  caucvglem6 7147  ser1cmp 7159  ser1cmp2 7162  cvgcmp2lem 7165  infcvgaux2 7205  infcvglem1 7206  georeclim 7225  fsum0diaglem1 7241  fsum0diag4 7246  ivthlem6 7271  ivthlem7 7272  erelem3 7306  efaddlem1 7323  efaddlem6 7328  efaddlem14 7336  efaddlem15 7337  efaddlem23 7345  ef1tllem 7366  ef01tllem2 7369  ef01tllem2OLD 7370  abspef01tlub 7380  efcnlem2 7405  efcn 7408  reeff1o 7411  subcost 7445  sinbndt 7450  cosbndt 7451  sin01bndlem2 7453  sin01bndlem3 7454  cos01bndlem2 7455  cos01bndlem3 7456  sin01gt0 7461  cos01gt0 7462  infpnlem2 7492  infxpidmlem10 7546  alephexp2 7571  opncld 7659  iincld 7664  clsidm 7683  ntridm 7684  clstop 7685  ntrtop 7686  ntrcls0 7692  cls0 7694  ntr0 7695  neiss2 7701  opnneiss 7717  metxp 7819  bl2in 7828  opni2 7850  lpbl 7865  methausi 7866  metcnpf 7868  metcnf 7869  lmnn 7920  lmuni 7936  bopcnlem3 7968  cmsss 7982  bcthlem16 7999  bcthlem18 8001  bcthlem19 8002  bcthlem21 8004  bcthlem24 8007  bcthlem33 8016  grp2inv 8063  vc0 8173  vcoprnelem 8182  vcoprne 8183  nvcni 8314  nvcni2 8315  nvcni3 8316  nvcnpi3 8407  nvcnpi4 8408  nmlno0lem 8438  nmblolbii 8444  ipasslem2 8476  ipasslem4 8478  ipasslem9 8483  minveclem9 8538  minveclem10 8539  minveclem14 8543  minveclem21 8550  minveclem24 8553  minveclem28 8557  htthlem10 8614  spwpr3OLD 8647  spwpr4OLD 8648  spwpr4aOLD 8649  sinperlem1 8671  sineq0 8698  shftefif1olem 8726  eff1i 8729  his6t 8950  normpyct 8998  shorth 9153  projlem8 9178  projlem13 9183  projlem26 9196  pjthlem10 9213  pjthlem11 9214  choc1 9276  pjspansnt 9485  osumlem3 9565  5oalem3 9586  homulid2t 9711  homco1t 9712  homulasst 9713  hoadddit 9714  hoadddirt 9715  unopnormt 9826  unoplint 9829  elnlfn2t 9838  adjt 9842  adj2t 9843  adjadjt 9845  adjvalvalt 9846  hmoplint 9851  homco2t 9886  nmlnop0ALT 9905  nmopunt 9924  nmbdoplb 9934  nmcoplb 9943  nmophm 9946  lnopcon 9948  nmbdfnlb 9963  nmcfnlb 9972  lnfncon 9975  nlelch 9979  riesz3 9980  cnlnadjlem6 9990  adjlnopt 10004  nmopco 10013  cnvbravalt 10028  hmopidmch 10064  pjssdif1 10088  hstle1t 10138  hstlet 10142  hstoht 10144  stles 10153  stadd 10158  stadd3 10160  strlem1 10162  strlem3a 10164  strlem5 10167  dmdbr5 10220  mdsl2b 10235  chrelat 10276  atcvatlem 10297  irredlem4 10305  mdsymlem5 10319  sumdmdi 10327  cdj3lem2 10347  cdj3lem2b 10349  ghomfo 10376  cayleythlem 10398  ompfl3 10412  infi1 10430  mslb1 10572  2wsms 10573  msra3 10574  iintlem1 10575  trnij 10580

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