![]() |
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 314 | . 2 ⊢ (𝜓 → (𝜑 ∧ 𝜓)) |
3 | mpanl1.2 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | |
4 | 2, 3 | sylan 283 | 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: mpanl12 436 ercnv 6558 rec11api 8712 divdiv23apzi 8724 recp1lt1 8858 divgt0i 8869 divge0i 8870 ltreci 8871 lereci 8872 lt2msqi 8873 le2msqi 8874 msq11i 8875 ltdiv23i 8885 fnn0ind 9371 elfzp1b 10099 elfzm1b 10100 sqrt11i 11143 sqrtmuli 11144 sqrtmsq2i 11146 sqrtlei 11147 sqrtlti 11148 |
Copyright terms: Public domain | W3C validator |