Theorem mpbii 168

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 135	. 2 ⊢ (φ → (ψ → χ))
4	1, 3	mpi 44	1 ⊢ (φ → χ)

Syntax hints:   → wi 2   ↔ wb 127

This theorem is referenced by:  elimh 571  zfext2 1087  ralcom2 1314  vtoclgf 1382  eqvinc 1407  moeq3 1432  mo2icl 1434  sbc2or 1454  eqimss 1548  ssex 1700  un00 1728  elimhyp 1790  elimhyp2v 1791  elimhyp3v 1792  keephyp 1794  keephyp3v 1795  sneqr 1856  preqr1 1872  preq12b 1874  prel12 1875  mosubop 1911  opthwiener 1914  iunpw 2040  syl5breq 2091  so 2152  ordtri3or 2230  eqelsuc 2307  onsucuni 2335  onuninsuc 2356  on0eqelt 2370  elxp5 2641  dfrel2 2660  tz6.12i 2847  fvco 2865  fvopabn 2873  fvopab2 2878  fvelrn 2883  abrexex 2912  isofrlem 2939  tfrlem11 2959  1st2val 3097  oaword1 3154  oalimcl 3162  nnmordi 3188  mapprc 3260  breng 3280  brdomg 3281  idssen 3309  xpsnen 3339  pw2en 3348  sbthlem5 3353  mapdom2lem 3388  ssenen 3399  phplem3 3405  ssfi 3430  fiint 3445  inf5 3472  rankel 3524  r1rankid 3537  rankonid 3538  rankr1id 3539  kmlem5 3584  oncardon 3627  oncardid 3628  iscard 3659  iscard2 3660  carduni 3664  alephnbtwn 3674  alephgeom 3687  cardaleph 3690  iscard3 3693  alephsson 3699  cardcf 3706  axrepndlem1 3738  axunndlem1 3741  axunnd 3742  axpowndlem2 3744  axpowndlem3 3745  axpowndlem4 3746  axpownd 3747  axregndlem2 3749  axinfndlem1 3751  axinfnd 3752  axacndlem4 3756  axacndlem5 3757  axacnd 3758  indpi 3828  recidpq 3865  ltaddpq 3873  muln0 4214  divneq0 4231  ltplus1t 4383  nnsub 4450  creur 4532  creui 4533  elnn0z 4574  elnnz1 4581  elnn0nn 4593  nn0ind 4612  nneo 4719  nnesq 4720  sqrlem6 4736  sqrlem12 4742  sqrth 4757  sqrcl 4758  sqr2irr 4782  replimt 4798  rere 4810  negre 4825  infxpidmlem10 4942  infxpidmlem11 4943  hlimcaui 5141  hsn0elch 5155  omlsilem 5249  pjch 5269  hsupclt 5308  chsupsn 5313  chj00 5408  chabs1t 5432  osum 5538  pjss1co 5633  atcvat4 5775

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128

metamath.org