Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mpdan | GIF version |
Description: An inference based on modus ponens. (Contributed by NM, 23-May-1999.) (Proof shortened by Wolf Lammen, 22-Nov-2012.) |
Ref | Expression |
---|---|
mpdan.1 | ⊢ (𝜑 → 𝜓) |
mpdan.2 | ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
Ref | Expression |
---|---|
mpdan | ⊢ (𝜑 → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 19 | . 2 ⊢ (𝜑 → 𝜑) | |
2 | mpdan.1 | . 2 ⊢ (𝜑 → 𝜓) | |
3 | mpdan.2 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | |
4 | 1, 2, 3 | syl2anc 408 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 107 |
This theorem is referenced by: mpidan 419 mpan2 421 mpjaodan 787 mpd3an3 1316 eueq2dc 2857 csbiegf 3043 difsnb 3663 reusv3i 4380 fvmpt3 5500 ffvelrnd 5556 fnressn 5606 fliftel1 5695 f1oiso2 5728 riota5f 5754 1stvalg 6040 2ndvalg 6041 brtpos2 6148 tfrlemibxssdm 6224 dom2lem 6666 php5 6752 nnfi 6766 xpfi 6818 supisoti 6897 ordiso2 6920 omp1eomlem 6979 onenon 7040 oncardval 7042 cardonle 7043 recidnq 7201 archnqq 7225 prarloclemarch2 7227 recexprlem1ssl 7441 recexprlem1ssu 7442 recexprlemss1l 7443 recexprlemss1u 7444 recexprlemex 7445 0idsr 7575 lep1 8603 suprlubex 8710 uz11 9348 xnegid 9642 eluzfz2 9812 fzsuc 9849 fzsuc2 9859 fzp1disj 9860 fzneuz 9881 fzp1nel 9884 exbtwnzlemex 10027 flhalf 10075 modqval 10097 frec2uzsucd 10174 frecuzrdgsuc 10187 uzsinds 10215 seq3p1 10235 seqp1cd 10239 expubnd 10350 iexpcyc 10397 binom2sub1 10406 hashennn 10526 shftfval 10593 shftcan1 10606 cjval 10617 reval 10621 imval 10622 cjmulrcl 10659 addcj 10663 absval 10773 resqrexlemdecn 10784 resqrexlemnmsq 10789 resqrexlemnm 10790 absneg 10822 abscj 10824 sqabsadd 10827 sqabssub 10828 ltabs 10859 dfabsmax 10989 negfi 10999 fsum3 11156 trirecip 11270 efval 11367 ege2le3 11377 efcan 11382 sinval 11409 cosval 11410 efi4p 11424 resin4p 11425 recos4p 11426 sincossq 11455 eirraplem 11483 iddvds 11506 1dvds 11507 bezoutlemstep 11685 coprmgcdb 11769 1idssfct 11796 exprmfct 11818 oddpwdclemdc 11851 phival 11889 setsn0fun 11996 cldval 12268 ntrfval 12269 clsfval 12270 neifval 12309 tx1cn 12438 ismet 12513 isxmet 12514 divcnap 12724 dvaddxxbr 12834 dvmulxxbr 12835 dvcoapbr 12840 bj-findis 13177 |
Copyright terms: Public domain | W3C validator |