![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mpbii | GIF version |
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.) |
Ref | Expression |
---|---|
mpbii.min | ⊢ 𝜓 |
mpbii.maj | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
mpbii | ⊢ (𝜑 → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpbii.min | . . 3 ⊢ 𝜓 | |
2 | 1 | a1i 9 | . 2 ⊢ (𝜑 → 𝜓) |
3 | mpbii.maj | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
4 | 2, 3 | mpbid 135 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 98 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: pm2.26dc 813 19.9ht 1532 ax11v2 1701 ax11v 1708 ax11ev 1709 equs5or 1711 nfsbxy 1818 nfsbxyt 1819 eqvisset 2565 vtoclgf 2612 eueq3dc 2715 mo2icl 2720 csbiegf 2890 un00 3263 sneqr 3531 preqr1 3539 preq12b 3541 prel12 3542 nfopd 3566 ssex 3894 iunpw 4211 nfimad 4677 dfrel2 4771 elxp5 4809 funsng 4946 cnvresid 4973 nffvd 5187 fnbrfvb 5214 funfvop 5279 acexmidlema 5503 tposf12 5884 recidnq 6491 ltaddnq 6505 ltadd1sr 6861 pncan3 7219 divcanap2 7659 ltp1 7810 ltm1 7812 recreclt 7866 nn0ind-raph 8355 2tnp1ge0ge0 9143 bdsepnft 10007 bdssex 10022 bj-inex 10027 bj-d0clsepcl 10049 bj-2inf 10062 bj-inf2vnlem2 10096 |
Copyright terms: Public domain | W3C validator |