Theorem mpbii 193

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

Hypotheses

Ref	Expression
mpbii.min	⊢ ψ
mpbii.maj	⊢ (φ → (ψ ↔ χ))

Assertion

Ref	Expression
mpbii	⊢ (φ → χ)

Proof of Theorem mpbii

Step	Hyp	Ref	Expression
1		mpbii.min	. 2 ⊢ ψ
2		mpbii.maj	. . 3 ⊢ (φ → (ψ ↔ χ))
3	2	biimpd 153	. 2 ⊢ (φ → (ψ → χ))
4	1, 3	mpi 44	1 ⊢ (φ → χ)

Syntax hints:   → wi 3   ↔ wb 146

This theorem is referenced by:  elimh 763  ax11v2 1213  ax11eq 1361  ax11el 1362  ax11inda 1369  zfext2 1459  ralcom2 1773  vtoclgf 1842  eqvinc 1879  moeq3 1917  mo2icl 1919  sbc2or 1954  eqimss 2105  un00 2302  elimhyp 2386  elimhyp2v 2387  elimhyp3v 2388  elimhyp4v 2389  elimdhyp 2391  keephyp2v 2393  keephyp3v 2394  sneqr 2473  preqr1 2477  preq12b 2479  prel12 2480  ssex 2714  opthwiener 2802  so 2859  rabsnt 2889  iunpw 2909  ordtri3or 2974  onsucuni 3080  onuninsuc 3103  on0eqelt 3119  elxp5 3446  dfrel2 3477  cnvresid 3561  tz6.12i 3732  fvelrnb 3751  fvelimab 3756  fvco 3765  fvopabn 3777  fvopab2 3782  abrexex 3851  isofrlem 3892  oprvalelrn 4030  1st2val 4085  2nd2val 4086  oaword1 4176  oneo 4202  idssen 4393  xpsnen 4421  pw2en 4432  sbthlem5 4437  mapdom2lem 4479  ssenen 4490  phplem2 4495  ssfi 4521  fiint 4540  abfii2 4542  infeq5 4601  rankel 4660  r1rankid 4674  rankonid 4675  rankr1id 4677  rankxpsuc 4695  kmlem5 4749  iscard 4833  iscard2 4834  carduni 4838  alephnbtwn 4848  alephgeom 4862  cardaleph 4865  iscard3 4868  alephsson 4874  alephfp 4880  alephval2 4882  alephval3 4883  axrepndlem1 4924  axunndlem1 4927  axunnd 4928  axpowndlem2 4930  axpowndlem3 4931  axpowndlem4 4932  axpownd 4933  axregndlem2 4935  axinfndlem1 4937  axinfnd 4938  axacndlem4 4942  axacndlem5 4943  axacnd 4944  indpi 5014  recidpq 5051  ltaddpq 5059  pncan3t 5357  1re 5415  divne0 5701  ltp1t 5775  ltm1t 5779  recrecltt 5858  elnn0z 6102  elnnz1 6110  elnn0nn 6126  nneo 6152  nn0ind-raph 6170  snunioolem 6355  nnesq 6600  sqrlem6 6616  sqrlem12 6622  sqrth 6637  sqr2irr 6667  rereb 6723  negreb 6738  faclbnd5 6898  efcltlem1 7254  sin01bndlem2 7418  cos01bndlem2 7420  sin01gt0 7426  cos01gt0 7427  infxpidmlem10 7512  infxpidmlem11 7513  subbas2 7595  cncnplem4 7727  bcthlem10 7958  sinhalfpilem 8617  hlimcaui 9045  hsn0elch 9059  omlsilem 9182  pjch 9203  chsupsn 9250  shs00 9311  chj00 9348  chabs1t 9377  osum 9526  osumcor2 9530  nonbool 9536  pjss1co 10029  atcvat4 10261  efilcp 10481  efilcp2 10486  cnfilca 10487

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