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 270 | . 2 ⊢ (𝜑 ∧ 𝜓) |
4 | mp4an.3 | . . 3 ⊢ 𝜒 | |
5 | mp4an.4 | . . 3 ⊢ 𝜃 | |
6 | 4, 5 | pm3.2i 270 | . 2 ⊢ (𝜒 ∧ 𝜃) |
7 | mp4an.5 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏) | |
8 | 3, 6, 7 | mp2an 422 | 1 ⊢ 𝜏 |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 107 |
This theorem is referenced by: 1lt2nq 7207 m1p1sr 7561 m1m1sr 7562 0lt1sr 7566 axi2m1 7676 mul4i 7903 add4i 7920 addsub4i 8051 muladdi 8164 lt2addi 8265 le2addi 8266 mulap0i 8410 divap0i 8513 divmuldivapi 8525 divmul13api 8526 divadddivapi 8527 divdivdivapi 8528 subrecapi 8592 8th4div3 8932 iap0 8936 fldiv4p1lem1div2 10071 sqrt2gt1lt2 10814 abs3lemi 10922 3dvds2dec 11552 flodddiv4 11620 nprmi 11794 sinhalfpilem 12861 |
Copyright terms: Public domain | W3C validator |