![]() |
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 147 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff set class |
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 2747 vtoclgf 2795 vtoclg1f 2796 eueq3dc 2911 mo2icl 2916 csbiegf 3100 un00 3469 sneqr 3760 preqr1 3768 preq12b 3770 prel12 3771 nfopd 3795 ssex 4140 exmidundif 4206 iunpw 4480 nfimad 4979 dfrel2 5079 funsng 5262 cnvresid 5290 nffvd 5527 fnbrfvb 5556 funfvop 5628 acexmidlema 5865 tposf12 6269 supsnti 7003 exmidonfinlem 7191 sucpw1ne3 7230 sucpw1nel3 7231 recidnq 7391 ltaddnq 7405 ltadd1sr 7774 suplocsrlempr 7805 pncan3 8163 divcanap2 8635 ltp1 8799 ltm1 8801 recreclt 8855 nn0ind-raph 9368 2tnp1ge0ge0 10298 fsumcnv 11440 fprodcnv 11628 ef01bndlem 11759 sin01gt0 11764 cos01gt0 11765 ltoddhalfle 11892 bezoutlemnewy 11991 isprm5 12136 nmznsg 13026 tangtx 14152 bdsepnft 14521 bdssex 14536 bj-inex 14541 bj-d0clsepcl 14559 bj-2inf 14572 bj-inf2vnlem2 14605 |
Copyright terms: Public domain | W3C validator |