![]() |
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 425 | . 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃) |
5 | 1, 4 | mpan 415 | 1 ⊢ (𝜒 → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem is referenced by: reuun1 3247 ordtri2orexmid 4268 opthreg 4301 ordtri2or2exmid 4316 fvtp1 5398 nq0m0r 6697 nq02m 6706 gt0srpr 6976 pitoregt0 7068 axcnre 7098 addgt0 7608 addgegt0 7609 addgtge0 7610 addge0 7611 addgt0i 7645 addge0i 7646 addgegt0i 7647 add20i 7649 mulge0i 7776 recextlem1 7797 recap0 7829 recdivap 7862 recgt1 8031 prodgt0i 8042 prodge0i 8043 iccshftri 9082 iccshftli 9084 iccdili 9086 icccntri 9088 mulexpzap 9602 expaddzap 9606 m1expeven 9609 iexpcyc 9665 amgm2 10131 sqnprm 10650 |
Copyright terms: Public domain | W3C validator |