Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mp3an2 | GIF version |
Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.) |
Ref | Expression |
---|---|
mp3an2.1 | ⊢ 𝜓 |
mp3an2.2 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
mp3an2 | ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mp3an2.1 | . 2 ⊢ 𝜓 | |
2 | mp3an2.2 | . . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
3 | 2 | 3expa 1198 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
4 | 1, 3 | mpanl2 433 | 1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 973 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 975 |
This theorem is referenced by: mp3anl2 1327 ordin 4368 ordsuc 4545 omv 6432 oeiv 6433 omv2 6442 1idprl 7545 muladd11 8045 negsub 8160 subneg 8161 ltaddneg 8336 muleqadd 8579 diveqap1 8615 conjmulap 8639 nnsub 8910 addltmul 9107 zltp1le 9259 gtndiv 9300 eluzp1m1 9503 xnn0le2is012 9816 divelunit 9952 fznatpl1 10025 flqbi2 10240 flqdiv 10270 frecfzen2 10376 nn0ennn 10382 faclbnd3 10670 shftfvalg 10775 ovshftex 10776 shftfval 10778 abs2dif 11063 cos2t 11706 sin01gt0 11717 cos01gt0 11718 demoivre 11728 demoivreALT 11729 omeo 11850 gcd0id 11927 sqgcd 11977 isprm3 12065 eulerthlemth 12179 pczpre 12244 pcrec 12255 setscom 12449 setsslid 12459 setsslnid 12460 abssinper 13526 lgs1 13704 |
Copyright terms: Public domain | W3C validator |