![]() |
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 434 | . 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃) |
5 | 1, 4 | mpan 424 | 1 ⊢ (𝜒 → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 |
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 is referenced by: reuun1 3432 ordtri2orexmid 4540 opthreg 4573 ordtri2or2exmid 4588 ontri2orexmidim 4589 fvtp1 5748 nq0m0r 7485 nq02m 7494 gt0srpr 7777 map2psrprg 7834 pitoregt0 7878 axcnre 7910 addgt0 8435 addgegt0 8436 addgtge0 8437 addge0 8438 addgt0i 8475 addge0i 8476 addgegt0i 8477 add20i 8479 mulge0i 8607 recextlem1 8638 recap0 8672 recdivap 8705 recgt1 8884 prodgt0i 8895 prodge0i 8896 iccshftri 10025 iccshftli 10027 iccdili 10029 icccntri 10031 mulexpzap 10591 expaddzap 10595 m1expeven 10598 iexpcyc 10656 amgm2 11159 ege2le3 11711 sqnprm 12168 lmres 14205 2logb9irrap 14852 |
Copyright terms: Public domain | W3C validator |