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 762  ax11v2 1210  ax11eq 1356  ax11el 1357  ax11inda 1364  zfext2 1454  ralcom2 1768  vtoclgf 1837  eqvinc 1874  moeq3 1912  mo2icl 1914  sbc2or 1948  eqimss 2099  un00 2296  elimhyp 2380  elimhyp2v 2381  elimhyp3v 2382  elimhyp4v 2383  elimdhyp 2385  keephyp2v 2387  keephyp3v 2388  sneqr 2468  preqr1 2472  preq12b 2474  prel12 2475  ssex 2709  opthwiener 2796  so 2855  rabsnt 2884  iunpw 2904  ordtri3or 2969  onsucuni 3075  onuninsuc 3098  on0eqelt 3114  elxp5 3440  dfrel2 3471  cnvresid 3555  tz6.12i 3726  fvelrnb 3745  fvelimab 3750  fvco 3759  fvopabn 3771  fvopab2 3776  abrexex 3845  isofrlem 3886  oprvalelrn 4024  1st2val 4079  2nd2val 4080  oaword1 4170  oneo 4196  idssen 4387  xpsnen 4415  pw2en 4426  sbthlem5 4431  mapdom2lem 4473  ssenen 4484  phplem2 4489  ssfi 4515  fiint 4534  abfii2 4536  infeq5 4593  rankel 4652  r1rankid 4666  rankonid 4667  rankr1id 4669  rankxpsuc 4687  kmlem5 4741  iscard 4825  iscard2 4826  carduni 4830  alephnbtwn 4840  alephgeom 4854  cardaleph 4857  iscard3 4860  alephsson 4866  alephfp 4872  alephval2 4874  alephval3 4875  axrepndlem1 4916  axunndlem1 4919  axunnd 4920  axpowndlem2 4922  axpowndlem3 4923  axpowndlem4 4924  axpownd 4925  axregndlem2 4927  axinfndlem1 4929  axinfnd 4930  axacndlem4 4934  axacndlem5 4935  axacnd 4936  indpi 5006  recidpq 5043  ltaddpq 5051  pncan3t 5349  1re 5407  divne0 5693  ltp1t 5767  ltm1t 5771  recrecltt 5850  elnn0z 6094  elnnz1 6102  elnn0nn 6118  nneo 6144  nn0ind-raph 6162  snunioolem 6347  nnesq 6592  sqrlem6 6608  sqrlem12 6614  sqrth 6629  sqr2irr 6659  rereb 6715  negreb 6730  faclbnd5 6890  efcltlem1 7246  sin01bndlem2 7410  cos01bndlem2 7412  sin01gt0 7418  cos01gt0 7419  infxpidmlem10 7504  infxpidmlem11 7505  subbas2 7587  cncnplem4 7716  bcthlem10 7942  sinhalfpilem 8598  hlimcaui 9027  hsn0elch 9041  omlsilem 9159  pjch 9180  chsupsn 9227  shs00 9288  chj00 9325  chabs1t 9354  osum 9503  osumcor2 9507  nonbool 9513  pjss1co 10002  atcvat4 10232  efilcp 10445  efilcp2 10450  cnfilca 10451

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