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 4370 ordsuc 4547 omv 6434 oeiv 6435 omv2 6444 1idprl 7552 muladd11 8052 negsub 8167 subneg 8168 ltaddneg 8343 muleqadd 8586 diveqap1 8622 conjmulap 8646 nnsub 8917 addltmul 9114 zltp1le 9266 gtndiv 9307 eluzp1m1 9510 xnn0le2is012 9823 divelunit 9959 fznatpl1 10032 flqbi2 10247 flqdiv 10277 frecfzen2 10383 nn0ennn 10389 faclbnd3 10677 shftfvalg 10782 ovshftex 10783 shftfval 10785 abs2dif 11070 cos2t 11713 sin01gt0 11724 cos01gt0 11725 demoivre 11735 demoivreALT 11736 omeo 11857 gcd0id 11934 sqgcd 11984 isprm3 12072 eulerthlemth 12186 pczpre 12251 pcrec 12262 setscom 12456 setsslid 12466 setsslnid 12467 abssinper 13561 lgs1 13739 |
Copyright terms: Public domain | W3C validator |