New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  mpbii GIF version

Theorem mpbii 202
 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
StepHypRef Expression
1 mpbii.min . . 3 ψ
21a1i 10 . 2 (φψ)
3 mpbii.maj . 2 (φ → (ψχ))
42, 3mpbid 201 1 (φχ)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 176 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8 This theorem depends on definitions:  df-bi 177 This theorem is referenced by:  elimh  922  ax11v2  1992  sbft  2025  ax11vALT  2097  ax11eq  2193  ax11el  2194  ax11inda  2200  ax11v2-o  2201  vtoclgf  2913  eueq3  3011  moeq3  3013  mo2icl  3015  sbc2or  3054  csbiegf  3176  un00  3586  elimhyp  3710  elimhyp2v  3711  elimhyp3v  3712  elimhyp4v  3713  elimdhyp  3715  keephyp2v  3717  keephyp3v  3718  sneqr  3872  unsneqsn  3887  preqr1  4124  preq12b  4127  lefinlteq  4463  proj2op  4601  nfopd  4605  phiall  4618  nfimad  4954  cnvresid  5166  nffvd  5335  tz6.12i  5348  fvelrnb  5365  fvelimab  5370  funfvop  5400  opbr1st  5501  opbr2nd  5502  bren  6030  idssen  6040  enadj  6060  ncvsq  6256
 Copyright terms: Public domain W3C validator