Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mpanr1 | GIF version |
Description: An inference based on modus ponens. (Contributed by NM, 3-May-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
Ref | Expression |
---|---|
mpanr1.1 | ⊢ 𝜓 |
mpanr1.2 | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
Ref | Expression |
---|---|
mpanr1 | ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpanr1.1 | . 2 ⊢ 𝜓 | |
2 | mpanr1.2 | . . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) | |
3 | 2 | anassrs 380 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
4 | 1, 3 | mpanl2 411 | 1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem is referenced by: mpanr12 415 axcnre 6955 rec11api 7729 divdiv23apzi 7741 recp1lt1 7865 divgt0i 7876 divge0i 7877 ltreci 7878 lereci 7879 lt2msqi 7880 le2msqi 7881 msq11i 7882 ltdiv23i 7892 ge0gtmnf 8736 sqrt11i 9728 sqrtmuli 9729 sqrtmsq2i 9731 sqrtlei 9732 sqrtlti 9733 |
Copyright terms: Public domain | W3C validator |