![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mpanl12 | GIF version |
Description: An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.) |
Ref | Expression |
---|---|
mpanl12.1 | ⊢ 𝜑 |
mpanl12.2 | ⊢ 𝜓 |
mpanl12.3 | ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
mpanl12 | ⊢ (𝜒 → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpanl12.2 | . 2 ⊢ 𝜓 | |
2 | mpanl12.1 | . . 3 ⊢ 𝜑 | |
3 | mpanl12.3 | . . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | |
4 | 2, 3 | mpanl1 426 | . 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃) |
5 | 1, 4 | mpan 416 | 1 ⊢ (𝜒 → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem is referenced by: reuun1 3297 ordtri2orexmid 4367 opthreg 4400 ordtri2or2exmid 4415 fvtp1 5547 nq0m0r 7112 nq02m 7121 gt0srpr 7391 pitoregt0 7483 axcnre 7513 addgt0 8023 addgegt0 8024 addgtge0 8025 addge0 8026 addgt0i 8063 addge0i 8064 addgegt0i 8065 add20i 8067 mulge0i 8194 recextlem1 8217 recap0 8249 recdivap 8282 recgt1 8455 prodgt0i 8466 prodge0i 8467 iccshftri 9561 iccshftli 9563 iccdili 9565 icccntri 9567 mulexpzap 10126 expaddzap 10130 m1expeven 10133 iexpcyc 10190 amgm2 10682 ege2le3 11126 sqnprm 11560 lmres 12115 |
Copyright terms: Public domain | W3C validator |