| 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 10551 flqdiv 10583 frecfzen2 10689 nn0ennn 10695 seqshft2g 10744 seqf1oglem1 10781 faclbnd3 11005 ccatrid 11184 shftfvalg 11379 ovshftex 11380 shftfval 11382 abs2dif 11667 cos2t 12312 sin01gt0 12324 cos01gt0 12325 demoivre 12335 demoivreALT 12336 omeo 12460 gcd0id 12551 sqgcd 12601 isprm3 12691 eulerthlemth 12805 pczpre 12871 pcrec 12882 setscom 13123 setsslid 13134 setsslnid 13135 mulgm1 13730 abssinper 15572 lgs1 15775 |
| Copyright terms: Public domain | W3C validator |