Theorem mpbii 209

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

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

This theorem is referenced by:  elimh 838  ax11v2 1423  ax11eq 1592  ax11el 1593  ax11inda 1600  axext3OLD 1705  ralcom2OLD 2079  vtoclgf 2178  eqvincOLD 2221  moeq3 2265  mo2icl 2267  sbc2or 2314  eqimssOLD 2499  un00 2731  elimhyp 2845  elimhyp2v 2846  elimhyp3v 2847  elimhyp4v 2848  elimdhyp 2850  keephyp2v 2852  keephyp3v 2853  sneqr 2969  preqr1 2974  preq12b 2976  prel12 2977  ssex 3270  opcom 3362  opthwiener 3369  so 3435  ordtri3or 3506  ordtri3orOLD 3507  on0eqel 3598  rabsnt 3632  iunpw 3669  onsucuni 3718  onuninsuci 3732  dfrel2 4169  dmsnop 4178  elxp5 4191  cnvresid 4299  tz6.12i 4509  fvelrnb 4530  fvelimab 4536  fvelimabOLD 4537  fvco 4547  fvopabn 4560  fvopab2 4565  abrexex 4647  isofrlem 4689  oprvelrn 4780  oaword1 5045  oneo 5071  idssen 5276  xpsnen 5305  pw2en 5316  ac6sfi 5320  sbthlem5 5325  mapdom2lem 5397  ssenen 5408  phplem2 5413  ssfi 5440  fiint 5460  abfii2 5462  ordiso 5493  infeq5 5536  rankel 5600  r1rankid 5614  rankonid 5615  rankr1id 5617  rankxpsuc 5635  omsublim 5683  kmlem5 5727  iscard 5801  iscard2 5802  carduni 5806  alephnbtwn 5812  alephgeom 5826  cardaleph 5829  iscard3 5832  alephsson 5838  alephfp 5844  alephval2 5846  alephval3 5847  nnacda 5884  axrepndlem1 5892  axunndlem1 5895  axunnd 5896  axpowndlem2 5898  axpowndlem3 5899  axpowndlem4 5900  axpownd 5901  axregndlem2 5903  axinfndlem1 5905  axinfnd 5906  axacndlem4 5910  axacndlem5 5911  axacnd 5912  indpi 5982  recidpq 6019  ltaddpq 6027  pncan3 6330  1re 6394  divne0i 6709  ltp1 6784  ltm1 6788  recreclt 6880  elnn0z 7151  elnnz1 7159  elnn0nn 7175  nneoi 7204  nn0ind-raph 7221  snunioolem 7378  nnesqi 7707  sqrlem6 7723  sqrlem12 7729  sqrthi 7744  sqr2irr 7774  negrebi 7840  faclbnd5 8000  elt3OLD 8453  egt2lt3 8454  sin01bndlem2 8529  cos01bndlem2 8531  sin01gt0 8537  cos01gt0 8538  infxpidmlem10 8625  infxpidmlem11 8626  subbas2 8710  cnpnei 8838  cncnplem4 8849  bcthlem10 9081  sinhalfpilem 9823  oprabopabf 9951  dif1enOLD 9967  findcard 9970  clint3 9977  fbssint 10071  hlimcauii 10531  hsn0elch 10545  omlsilem 10669  pjchi 10690  chsupsn 10737  shs00i 10798  chj00i 10835  chabs1 10864  osumi 11013  osumcor2i 11017  nonbooli 11023  pjss1coi 11527  atcvat4i 11761  bnj90OLD 12238  bnj139 12263  bnj898 12607  bnj1337 12856  bnj609 13098  bnj854 13106  bnj981 13148  bnj1015 13167  bnj1148 13226  bnj1152 13229  bnj1154 13230  bnj1326 13288  bnj1329 13289  bnj1418 13321  isprm2lem 13566  dfon2lem3 13642  dfon2lem7 13646  distel 13661  cbicplem 14234  cur1vald 14273  trooo 14481  trinv 14482  efilcp 14636  efilcp2 14640  cnfilca 14641  cntrsetlem 14709  ordisoOLD 15056  omsublimOLD 15078  cncls 15101  cnntr 15102  compfipin0lem 15117  compfipin0 15118  fcluscomplem 15302  inficl 15439  rddif 15480  absrdbnd 15481  ismtyhmeolem 15632  heiborlem35 15671  bfplem9 15688  pcoval2 15757  pcorev 15769  isdivrng2 15793  0ring 15857  keridl 15862

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 163

Copyright terms: Public domain