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 772 mpd3an3 1301 eueq2dc 2830 csbiegf 3013 difsnb 3633 reusv3i 4350 fvmpt3 5468 ffvelrnd 5524 fnressn 5574 fliftel1 5663 f1oiso2 5696 riota5f 5722 1stvalg 6008 2ndvalg 6009 brtpos2 6116 tfrlemibxssdm 6192 dom2lem 6634 php5 6720 nnfi 6734 xpfi 6786 supisoti 6865 ordiso2 6888 omp1eomlem 6947 onenon 7008 oncardval 7010 cardonle 7011 recidnq 7169 archnqq 7193 prarloclemarch2 7195 recexprlem1ssl 7409 recexprlem1ssu 7410 recexprlemss1l 7411 recexprlemss1u 7412 recexprlemex 7413 0idsr 7543 lep1 8571 suprlubex 8678 uz11 9316 xnegid 9610 eluzfz2 9780 fzsuc 9817 fzsuc2 9827 fzp1disj 9828 fzneuz 9849 fzp1nel 9852 exbtwnzlemex 9995 flhalf 10043 modqval 10065 frec2uzsucd 10142 frecuzrdgsuc 10155 uzsinds 10183 seq3p1 10203 seqp1cd 10207 expubnd 10318 iexpcyc 10365 binom2sub1 10374 hashennn 10494 shftfval 10561 shftcan1 10574 cjval 10585 reval 10589 imval 10590 cjmulrcl 10627 addcj 10631 absval 10741 resqrexlemdecn 10752 resqrexlemnmsq 10757 resqrexlemnm 10758 absneg 10790 abscj 10792 sqabsadd 10795 sqabssub 10796 ltabs 10827 dfabsmax 10957 negfi 10967 fsum3 11124 trirecip 11238 efval 11294 ege2le3 11304 efcan 11309 sinval 11336 cosval 11337 efi4p 11351 resin4p 11352 recos4p 11353 sincossq 11382 eirraplem 11410 iddvds 11433 1dvds 11434 bezoutlemstep 11612 coprmgcdb 11696 1idssfct 11723 exprmfct 11745 oddpwdclemdc 11778 phival 11816 setsn0fun 11923 cldval 12195 ntrfval 12196 clsfval 12197 neifval 12236 tx1cn 12365 ismet 12440 isxmet 12441 divcnap 12651 dvaddxxbr 12761 dvmulxxbr 12762 dvcoapbr 12767 bj-findis 13104 |
Copyright terms: Public domain | W3C validator |