| 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 1229 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
| 4 | 1, 3 | mpanl2 435 | 1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
| Colors of variables: wff set class |
| Syntax hints: → wi 4 ∧ wa 104 ∧ w3a 1004 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
| This theorem depends on definitions: df-bi 117 df-3an 1006 |
| This theorem is referenced by: mp3anl2 1368 ordin 4482 ordsuc 4661 omv 6623 oeiv 6624 omv2 6633 1idprl 7810 muladd11 8312 negsub 8427 subneg 8428 ltaddneg 8604 muleqadd 8848 diveqap1 8885 conjmulap 8909 nnsub 9182 addltmul 9381 zltp1le 9534 gtndiv 9575 eluzp1m1 9780 xnn0le2is012 10101 divelunit 10237 fznatpl1 10311 flqbi2 10552 flqdiv 10584 frecfzen2 10690 nn0ennn 10696 seqshft2g 10745 seqf1oglem1 10782 faclbnd3 11006 ccatrid 11188 shftfvalg 11396 ovshftex 11397 shftfval 11399 abs2dif 11684 cos2t 12329 sin01gt0 12341 cos01gt0 12342 demoivre 12352 demoivreALT 12353 omeo 12477 gcd0id 12568 sqgcd 12618 isprm3 12708 eulerthlemth 12822 pczpre 12888 pcrec 12899 setscom 13140 setsslid 13151 setsslnid 13152 mulgm1 13747 abssinper 15589 lgs1 15792 |
| Copyright terms: Public domain | W3C validator |