![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mp3an12 | GIF version |
Description: An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.) |
Ref | Expression |
---|---|
mp3an12.1 | ⊢ 𝜑 |
mp3an12.2 | ⊢ 𝜓 |
mp3an12.3 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
mp3an12 | ⊢ (𝜒 → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mp3an12.2 | . 2 ⊢ 𝜓 | |
2 | mp3an12.1 | . . 3 ⊢ 𝜑 | |
3 | mp3an12.3 | . . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
4 | 2, 3 | mp3an1 1334 | . 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃) |
5 | 1, 4 | mpan 424 | 1 ⊢ (𝜒 → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 979 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 df-3an 981 |
This theorem is referenced by: mp3an12i 1351 ceqsralv 2782 brelrn 4874 funpr 5282 fpm 6698 ener 6796 ltaddnq 7423 ltadd1sr 7792 map2psrprg 7821 mul02 8361 ltapi 8610 div0ap 8676 divclapzi 8721 divcanap1zi 8722 divcanap2zi 8723 divrecapzi 8724 divcanap3zi 8725 divcanap4zi 8726 divassapzi 8736 divmulapzi 8737 divdirapzi 8738 redivclapzi 8752 ltm1 8820 mulgt1 8837 recgt1i 8872 recreclt 8874 ltmul1i 8894 ltdiv1i 8895 ltmuldivi 8896 ltmul2i 8897 lemul1i 8898 lemul2i 8899 cju 8935 nnge1 8959 nngt0 8961 nnrecgt0 8974 elnnnn0c 9238 elnnz1 9293 recnz 9363 eluzsubi 9572 ge0gtmnf 9840 m1expcl2 10559 1exp 10566 m1expeven 10584 expubnd 10594 iexpcyc 10642 expnbnd 10661 expnlbnd 10662 remim 10886 imval2 10920 cjdivapi 10961 absdivapzi 11180 fprodge1 11664 ef01bndlem 11781 sin01gt0 11786 cos01gt0 11787 cos12dec 11792 absefib 11795 efieq1re 11796 zeo3 11890 evend2 11911 cnbl0 14417 reeff1olem 14575 sincosq1sgn 14630 sincosq3sgn 14632 sincosq4sgn 14633 rpelogb 14750 lgsdir2lem2 14813 |
Copyright terms: Public domain | W3C validator |