![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mp2b | GIF version |
Description: A double modus ponens inference. (Contributed by Mario Carneiro, 24-Jan-2013.) |
Ref | Expression |
---|---|
mp2b.1 | ⊢ 𝜑 |
mp2b.2 | ⊢ (𝜑 → 𝜓) |
mp2b.3 | ⊢ (𝜓 → 𝜒) |
Ref | Expression |
---|---|
mp2b | ⊢ 𝜒 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mp2b.1 | . . 3 ⊢ 𝜑 | |
2 | mp2b.2 | . . 3 ⊢ (𝜑 → 𝜓) | |
3 | 1, 2 | ax-mp 7 | . 2 ⊢ 𝜓 |
4 | mp2b.3 | . 2 ⊢ (𝜓 → 𝜒) | |
5 | 3, 4 | ax-mp 7 | 1 ⊢ 𝜒 |
Colors of variables: wff set class |
Syntax hints: → wi 4 |
This theorem was proved from axioms: ax-mp 7 |
This theorem is referenced by: eqvinc 2726 2ordpr 4295 regexmid 4306 ordsoexmid 4333 reg3exmid 4350 intasym 4759 relcoi1 4899 funres11 5022 cnvresid 5024 mpt2fvex 5880 df1st2 5891 df2nd2 5892 dftpos4 5932 tposf12 5938 frecabcl 6068 xpcomco 6391 ominf 6452 djuin 6556 rec1nq 6699 halfnqq 6714 caucvgsrlemasr 7080 axresscn 7142 0re 7233 gtso 7309 cnegexlem2 7403 uzn0 8767 indstr 8814 dfioo2 9125 hashinfuni 9853 hashp1i 9886 cnrecnv 9998 rexanuz 10075 climdm 10335 lcmgcdlem 10666 3prm 10717 sqpweven 10760 2sqpwodd 10761 qnumval 10770 qdenval 10771 xpnnen 10814 |
Copyright terms: Public domain | W3C validator |