Theorem mpbii 148

Description: An inference from a nested biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 25-Oct-2012.)

Hypotheses

Ref	Expression
mpbii.min	⊢ 𝜓
mpbii.maj	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
mpbii	⊢ (𝜑 → 𝜒)

Proof of Theorem mpbii

Step	Hyp	Ref	Expression
1		mpbii.min	. . 3 ⊢ 𝜓
2	1	a1i 9	. 2 ⊢ (𝜑 → 𝜓)
3		mpbii.maj	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	2, 3	mpbid 147	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.26dc  907  orandc  939  19.9ht  1641  ax11v2  1820  ax11v  1827  ax11ev  1828  equs5or  1830  nfsbxy  1942  nfsbxyt  1943  nfabdw  2338  eqvisset  2749  vtoclgf  2797  vtoclg1f  2798  eueq3dc  2913  mo2icl  2918  csbiegf  3102  un00  3471  sneqr  3762  preqr1  3770  preq12b  3772  prel12  3773  nfopd  3797  ssex  4142  exmidundif  4208  iunpw  4482  nfimad  4981  dfrel2  5081  funsng  5264  cnvresid  5292  nffvd  5529  fnbrfvb  5558  funfvop  5630  acexmidlema  5868  tposf12  6272  supsnti  7006  exmidonfinlem  7194  sucpw1ne3  7233  sucpw1nel3  7234  recidnq  7394  ltaddnq  7408  ltadd1sr  7777  suplocsrlempr  7808  pncan3  8167  divcanap2  8639  ltp1  8803  ltm1  8805  recreclt  8859  nn0ind-raph  9372  2tnp1ge0ge0  10303  fsumcnv  11447  fprodcnv  11635  ef01bndlem  11766  sin01gt0  11771  cos01gt0  11772  ltoddhalfle  11900  bezoutlemnewy  11999  isprm5  12144  nmznsg  13078  tangtx  14344  bdsepnft  14724  bdssex  14739  bj-inex  14744  bj-d0clsepcl  14762  bj-2inf  14775  bj-inf2vnlem2  14808