![]() |
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 297 | . 2 ⊢ (ψ → (φ ∧ ψ)) |
3 | mpanl1.2 | . 2 ⊢ (((φ ∧ ψ) ∧ χ) → θ) | |
4 | 2, 3 | sylan 267 | 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: mpanl12 412 ercnv 6063 rec11api 7511 divdiv23apzi 7523 recp1lt1 7646 divgt0i 7657 divge0i 7658 ltreci 7659 lereci 7660 lt2msqi 7661 le2msqi 7662 msq11i 7663 ltdiv23i 7673 fnn0ind 8130 elfzp1b 8729 elfzm1b 8730 |
Copyright terms: Public domain | W3C validator |