![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mp4an | GIF version |
Description: An inference based on modus ponens. (Contributed by Jeff Madsen, 15-Jun-2011.) |
Ref | Expression |
---|---|
mp4an.1 | ⊢ 𝜑 |
mp4an.2 | ⊢ 𝜓 |
mp4an.3 | ⊢ 𝜒 |
mp4an.4 | ⊢ 𝜃 |
mp4an.5 | ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏) |
Ref | Expression |
---|---|
mp4an | ⊢ 𝜏 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mp4an.1 | . . 3 ⊢ 𝜑 | |
2 | mp4an.2 | . . 3 ⊢ 𝜓 | |
3 | 1, 2 | pm3.2i 266 | . 2 ⊢ (𝜑 ∧ 𝜓) |
4 | mp4an.3 | . . 3 ⊢ 𝜒 | |
5 | mp4an.4 | . . 3 ⊢ 𝜃 | |
6 | 4, 5 | pm3.2i 266 | . 2 ⊢ (𝜒 ∧ 𝜃) |
7 | mp4an.5 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏) | |
8 | 3, 6, 7 | mp2an 417 | 1 ⊢ 𝜏 |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia3 106 |
This theorem is referenced by: 1lt2nq 6647 m1p1sr 6988 m1m1sr 6989 0lt1sr 6993 axi2m1 7092 mul4i 7312 add4i 7329 addsub4i 7460 muladdi 7569 lt2addi 7667 le2addi 7668 mulap0i 7802 divap0i 7904 divmuldivapi 7916 divmul13api 7917 divadddivapi 7918 divdivdivapi 7919 8th4div3 8306 iap0 8310 fldiv4p1lem1div2 9376 sqrt2gt1lt2 10062 abs3lemi 10170 3dvds2dec 10399 flodddiv4 10467 nprmi 10639 |
Copyright terms: Public domain | W3C validator |