![]() |
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 272 | . 2 ⊢ (𝜑 ∧ 𝜓) |
4 | mp4an.3 | . . 3 ⊢ 𝜒 | |
5 | mp4an.4 | . . 3 ⊢ 𝜃 | |
6 | 4, 5 | pm3.2i 272 | . 2 ⊢ (𝜒 ∧ 𝜃) |
7 | mp4an.5 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏) | |
8 | 3, 6, 7 | mp2an 426 | 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-ia3 108 |
This theorem is referenced by: 1lt2nq 7405 m1p1sr 7759 m1m1sr 7760 0lt1sr 7764 axi2m1 7874 mul4i 8105 add4i 8122 addsub4i 8253 muladdi 8366 lt2addi 8467 le2addi 8468 mulap0i 8613 divap0i 8717 divmuldivapi 8729 divmul13api 8730 divadddivapi 8731 divdivdivapi 8732 subrecapi 8797 8th4div3 9138 iap0 9142 fldiv4p1lem1div2 10305 sqrt2gt1lt2 11058 abs3lemi 11166 3dvds2dec 11871 flodddiv4 11939 nprmi 12124 sinhalfpilem 14215 cos0pilt1 14276 lgsdir2lem1 14432 lgsdir2lem5 14436 m1lgs 14455 |
Copyright terms: Public domain | W3C validator |