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 5 | . 2 ⊢ 𝜓 |
4 | mp2b.3 | . 2 ⊢ (𝜓 → 𝜒) | |
5 | 3, 4 | ax-mp 5 | 1 ⊢ 𝜒 |
Colors of variables: wff set class |
Syntax hints: → wi 4 |
This theorem was proved from axioms: ax-mp 5 |
This theorem is referenced by: eqvinc 2808 2ordpr 4439 regexmid 4450 ordsoexmid 4477 reg3exmid 4494 intasym 4923 relcoi1 5070 funres11 5195 cnvresid 5197 mpofvex 6101 df1st2 6116 df2nd2 6117 dftpos4 6160 tposf12 6166 frecabcl 6296 xp01disjl 6331 xpcomco 6720 ominf 6790 sbthlem2 6846 djuunr 6951 eldju 6953 ctssdccl 6996 ctssdclemr 6997 omct 7002 ctssexmid 7024 rec1nq 7203 halfnqq 7218 caucvgsrlemasr 7598 axresscn 7668 0re 7766 gtso 7843 cnegexlem2 7938 uzn0 9341 indstr 9388 dfioo2 9757 fnn0nninf 10210 hashinfuni 10523 hashp1i 10556 cnrecnv 10682 rexanuz 10760 xrmaxiflemcom 11018 climdm 11064 sumsnf 11178 tanvalap 11415 egt2lt3 11486 lcmgcdlem 11758 3prm 11809 sqpweven 11853 2sqpwodd 11854 qnumval 11863 qdenval 11864 xpnnen 11907 ennnfonelemhdmp1 11922 ennnfonelemss 11923 ennnfonelemnn0 11935 qnnen 11944 unct 11954 structcnvcnv 11975 setsslid 12009 tgrest 12338 lmbr2 12383 cnptoprest 12408 lmff 12418 tx1cn 12438 tx2cn 12439 cnblcld 12704 tgioo 12715 pilem1 12860 efhalfpi 12880 coseq0negpitopi 12917 isomninnlem 13225 |
Copyright terms: Public domain | W3C validator |