![]() |
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 7383 m1p1sr 7737 m1m1sr 7738 0lt1sr 7742 axi2m1 7852 mul4i 8082 add4i 8099 addsub4i 8230 muladdi 8343 lt2addi 8444 le2addi 8445 mulap0i 8589 divap0i 8693 divmuldivapi 8705 divmul13api 8706 divadddivapi 8707 divdivdivapi 8708 subrecapi 8773 8th4div3 9114 iap0 9118 fldiv4p1lem1div2 10278 sqrt2gt1lt2 11029 abs3lemi 11137 3dvds2dec 11841 flodddiv4 11909 nprmi 12094 sinhalfpilem 13845 cos0pilt1 13906 lgsdir2lem1 14062 lgsdir2lem5 14066 |
Copyright terms: Public domain | W3C validator |