Theorem mpbii 193

Description: An inference from a nested biconditional, related to modus ponens.

Hypotheses

Ref	Expression
mpbii.min	|- ps
mpbii.maj	|- (ph -> (ps <-> ch))

Assertion

Ref	Expression
mpbii	|- (ph -> ch)

Proof of Theorem mpbii

Step	Hyp	Ref	Expression
1		mpbii.min	. 2 |- ps
2		mpbii.maj	. . 3 |- (ph -> (ps <-> ch))
3	2	biimpd 153	. 2 |- (ph -> (ps -> ch))
4	1, 3	mpi 44	1 |- (ph -> ch)

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

This theorem is referenced by:  elimh 761  ax11v2 1199  ax11eq 1340  ax11el 1341  ax11inda 1348  zfext2 1438  ralcom2 1752  vtoclgf 1821  eqvinc 1855  moeq3 1893  mo2icl 1895  sbc2or 1929  eqimss 2080  un00 2277  elimhyp 2361  elimhyp2v 2362  elimhyp3v 2363  elimhyp4v 2364  elimdhyp 2366  keephyp2v 2368  keephyp3v 2369  sneqr 2447  preqr1 2451  preq12b 2453  prel12 2454  ssex 2687  opthwiener 2770  so 2828  rabsnt 2857  iunpw 2877  ordtri3or 2942  onsucuni 3048  onuninsuc 3071  on0eqelt 3087  elxp5 3403  dfrel2 3431  cnvresid 3509  tz6.12i 3680  fvelrnb 3699  fvelimab 3704  fvco 3713  fvopabn 3725  fvopab2 3730  abrexex 3799  isofrlem 3840  oprvalelrn 3978  1st2val 4033  2nd2val 4034  oaword1 4124  oneo 4150  idssen 4341  xpsnen 4369  pw2en 4380  sbthlem5 4385  mapdom2lem 4425  ssenen 4436  phplem2 4441  ssfi 4467  fiint 4486  abfii2 4488  infeq5 4545  rankel 4604  r1rankid 4618  rankonid 4619  rankr1id 4621  rankxpsuc 4639  kmlem5 4693  iscard 4776  iscard2 4777  carduni 4781  alephnbtwn 4791  alephgeom 4805  cardaleph 4808  iscard3 4811  alephsson 4817  alephfp 4823  alephval2 4825  alephval3 4826  axrepndlem1 4867  axunndlem1 4870  axunnd 4871  axpowndlem2 4873  axpowndlem3 4874  axpowndlem4 4875  axpownd 4876  axregndlem2 4878  axinfndlem1 4880  axinfnd 4881  axacndlem4 4885  axacndlem5 4886  axacnd 4887  indpi 4957  recidpq 4994  ltaddpq 5002  pncan3t 5300  1re 5358  divne0 5644  ltp1t 5718  ltm1t 5722  recrecltt 5801  elnn0z 6045  elnnz1 6053  elnn0nn 6069  nneo 6095  nn0ind-raph 6113  snunioolem 6298  nnesq 6543  sqrlem6 6559  sqrlem12 6565  sqrth 6580  sqr2irr 6610  rereb 6666  negreb 6681  faclbnd5 6841  efcltlem1 7197  sin01bndlem2 7361  cos01bndlem2 7363  sin01gt0 7369  cos01gt0 7370  infxpidmlem10 7455  infxpidmlem11 7456  subbas2 7538  cncnplem4 7664  bcthlem10 7890  sinhalfpilem 8511  efilcp 8795  efilcp2 8800  cnfilca 8801  hlimcaui 9257  hsn0elch 9271  omlsilem 9373  pjch 9394  chsupsn 9441  shs00 9502  chj00 9539  chabs1t 9568  osum 9717  osumcor2 9721  nonbool 9727  pjss1co 10216  atcvat4 10446

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