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 398 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
4 | 1, 3 | mpanl2 432 | 1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem is referenced by: mpanr12 436 axcnre 7802 rec11api 8627 divdiv23apzi 8639 recp1lt1 8771 divgt0i 8782 divge0i 8783 ltreci 8784 lereci 8785 lt2msqi 8786 le2msqi 8787 msq11i 8788 ltdiv23i 8798 ge0gtmnf 9728 sqrt11i 11036 sqrtmuli 11037 sqrtmsq2i 11039 sqrtlei 11040 sqrtlti 11041 cos01gt0 11663 |
Copyright terms: Public domain | W3C validator |