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 146 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: pm2.26dc 897 orandc 928 19.9ht 1628 ax11v2 1807 ax11v 1814 ax11ev 1815 equs5or 1817 nfsbxy 1929 nfsbxyt 1930 nfabdw 2325 eqvisset 2731 vtoclgf 2779 vtoclg1f 2780 eueq3dc 2895 mo2icl 2900 csbiegf 3083 un00 3450 sneqr 3734 preqr1 3742 preq12b 3744 prel12 3745 nfopd 3769 ssex 4113 exmidundif 4179 iunpw 4452 nfimad 4949 dfrel2 5048 funsng 5228 cnvresid 5256 nffvd 5492 fnbrfvb 5521 funfvop 5591 acexmidlema 5827 tposf12 6228 supsnti 6961 exmidonfinlem 7140 sucpw1ne3 7179 sucpw1nel3 7180 recidnq 7325 ltaddnq 7339 ltadd1sr 7708 suplocsrlempr 7739 pncan3 8097 divcanap2 8567 ltp1 8730 ltm1 8732 recreclt 8786 nn0ind-raph 9299 2tnp1ge0ge0 10226 fsumcnv 11364 fprodcnv 11552 ef01bndlem 11683 sin01gt0 11688 cos01gt0 11689 ltoddhalfle 11815 bezoutlemnewy 11914 isprm5 12053 tangtx 13306 bdsepnft 13610 bdssex 13625 bj-inex 13630 bj-d0clsepcl 13648 bj-2inf 13661 bj-inf2vnlem2 13694 |
Copyright terms: Public domain | W3C validator |