Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mpanl1 | GIF version |
Description: An inference based on modus ponens. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Wolf Lammen, 7-Apr-2013.) |
Ref | Expression |
---|---|
mpanl1.1 | ⊢ 𝜑 |
mpanl1.2 | ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
mpanl1 | ⊢ ((𝜓 ∧ 𝜒) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpanl1.1 | . . 3 ⊢ 𝜑 | |
2 | 1 | jctl 312 | . 2 ⊢ (𝜓 → (𝜑 ∧ 𝜓)) |
3 | mpanl1.2 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | |
4 | 2, 3 | sylan 281 | 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: mpanl12 432 ercnv 6418 rec11api 8481 divdiv23apzi 8493 recp1lt1 8625 divgt0i 8636 divge0i 8637 ltreci 8638 lereci 8639 lt2msqi 8640 le2msqi 8641 msq11i 8642 ltdiv23i 8652 fnn0ind 9135 elfzp1b 9845 elfzm1b 9846 sqrt11i 10872 sqrtmuli 10873 sqrtmsq2i 10875 sqrtlei 10876 sqrtlti 10877 |
Copyright terms: Public domain | W3C validator |