![]() |
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 145 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 103 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: pm2.26dc 847 orandc 881 19.9ht 1573 ax11v2 1743 ax11v 1750 ax11ev 1751 equs5or 1753 nfsbxy 1861 nfsbxyt 1862 eqvisset 2619 vtoclgf 2667 eueq3dc 2776 mo2icl 2781 csbiegf 2956 un00 3307 sneqr 3573 preqr1 3581 preq12b 3583 prel12 3584 nfopd 3608 ssex 3936 exmidundif 3992 iunpw 4258 nfimad 4728 dfrel2 4822 funsng 4997 cnvresid 5025 nffvd 5240 fnbrfvb 5268 funfvop 5333 acexmidlema 5556 tposf12 5940 supsnti 6514 recidnq 6722 ltaddnq 6736 ltadd1sr 7092 pncan3 7460 divcanap2 7912 ltp1 8066 ltm1 8068 recreclt 8122 nn0ind-raph 8622 2tnp1ge0ge0 9460 ltoddhalfle 10525 bezoutlemnewy 10617 bdsepnft 10970 bdssex 10985 bj-inex 10990 bj-d0clsepcl 11012 bj-2inf 11025 bj-inf2vnlem2 11058 |
Copyright terms: Public domain | W3C validator |