Theorem mpbii 191

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 151	. 2 |- (ph -> (ps -> ch))
4	1, 3	mpi 44	1 |- (ph -> ch)

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

This theorem is referenced by:  elimh 769  ax11v2 1252  ax11eq 1402  ax11el 1403  ax11inda 1410  axext3 1502  ralcom2 1822  vtoclgf 1892  eqvinc 1929  moeq3 1967  mo2icl 1969  sbc2or 2006  eqimss 2161  un00 2359  elimhyp 2447  elimhyp2v 2448  elimhyp3v 2449  elimhyp4v 2450  elimdhyp 2452  keephyp2v 2454  keephyp3v 2455  sneqr 2542  preqr1 2546  preq12b 2548  prel12 2549  ssex 2793  opcom 2877  opthwiener 2884  so 2943  ordtri3or 3007  on0eqel 3087  rabsnt 3117  iunpw 3137  onsucuni 3182  onuninsuci 3194  dfrel2 3569  elxp5 3586  cnvresid 3674  tz6.12i 3852  fvelrnb 3871  fvelimab 3876  fvco 3885  fvopabn 3897  fvopab2 3902  abrexex 3974  isofrlem 4015  oprvelrn 4100  oaword1 4322  oneo 4348  idssen 4547  xpsnen 4576  pw2en 4587  ac6sfi 4591  sbthlem5 4596  mapdom2lem 4640  ssenen 4651  phplem2 4656  ssfi 4683  fiint 4703  abfii2 4705  infeq5 4766  rankel 4826  r1rankid 4840  rankonid 4841  rankr1id 4843  rankxpsuc 4861  kmlem5 4915  iscard 5003  iscard2 5004  carduni 5008  alephnbtwn 5018  alephgeom 5032  cardaleph 5035  iscard3 5038  alephsson 5044  alephfp 5050  alephval2 5052  alephval3 5053  nnacda 5090  axrepndlem1 5098  axunndlem1 5101  axunnd 5102  axpowndlem2 5104  axpowndlem3 5105  axpowndlem4 5106  axpownd 5107  axregndlem2 5109  axinfndlem1 5111  axinfnd 5112  axacndlem4 5116  axacndlem5 5117  axacnd 5118  indpi 5188  recidpq 5225  ltaddpq 5233  pncan3 5531  1re 5589  divne0i 5876  ltp1 5951  ltm1 5955  recreclt 6047  elnn0z 6315  elnnz1 6323  elnn0nn 6339  nneoi 6368  nn0ind-raph 6385  snunioolem 6541  nnesqi 6863  sqrlem6 6879  sqrlem12 6885  sqrthi 6900  sqr2irr 6930  negrebi 6996  faclbnd5 7156  elt3OLD 7601  egt2lt3 7602  sin01bndlem2 7677  cos01bndlem2 7679  sin01gt0 7685  cos01gt0 7686  infxpidmlem10 7773  infxpidmlem11 7774  subbas2 7857  cncnplem4 7987  bcthlem10 8219  sinhalfpilem 8946  hlimcauii 9382  hsn0elch 9396  omlsilem 9520  pjchi 9541  chsupsn 9588  shs00i 9649  chj00i 9686  chabs1 9715  osumi 9864  osumcor2i 9868  nonbooli 9874  pjss1coi 10371  atcvat4i 10606  clint3 11002  efilcp 11083  efilcp2 11087  cnfilca 11088  ordiso 11426  omsublim 11448  cnpnei 11472  cncls 11473  cnntr 11474  compfipin0lem 11492  compfipin0 11493  fbssint 11626  fcluscomplem 11732  oprabopabf 11807  dif1en 11833  inficl 11849  rddif 11869  absrdbnd 11870  ismtyhmeolem 12006  heiborlem35 12045  bfplem9 12062

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 145

Copyright terms: Public domain