![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mp3an23 | GIF version |
Description: An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.) |
Ref | Expression |
---|---|
mp3an23.1 | ⊢ 𝜓 |
mp3an23.2 | ⊢ 𝜒 |
mp3an23.3 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
mp3an23 | ⊢ (𝜑 → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mp3an23.1 | . 2 ⊢ 𝜓 | |
2 | mp3an23.2 | . . 3 ⊢ 𝜒 | |
3 | mp3an23.3 | . . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
4 | 2, 3 | mp3an3 1326 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜃) |
5 | 1, 4 | mpan2 425 | 1 ⊢ (𝜑 → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 978 |
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 980 |
This theorem is referenced by: sbciegf 2994 ac6sfi 6891 dju0en 7206 1qec 7365 ltaddnq 7384 halfnqq 7387 1idsr 7745 pn0sr 7748 ltm1sr 7754 muleqadd 8601 halfcl 9121 rehalfcl 9122 half0 9123 2halves 9124 halfpos2 9125 halfnneg2 9127 halfaddsub 9129 nneoor 9331 zeo 9334 fztp 10051 modqfrac 10310 iexpcyc 10597 bcn2 10715 bcpasc 10717 imre 10831 reim 10832 crim 10838 addcj 10871 imval2 10874 sinf 11683 efi4p 11696 resin4p 11697 recos4p 11698 sinneg 11705 efival 11711 cosadd 11716 sinmul 11723 sinbnd 11731 cosbnd 11732 ef01bndlem 11735 sin01bnd 11736 cos01bnd 11737 sin01gt0 11740 cos01gt0 11741 sin02gt0 11742 odd2np1lem 11847 odd2np1 11848 pythagtriplem12 12245 pockthi 12326 mopnex 13638 sincosq1lem 13879 sincosq2sgn 13881 sincosq3sgn 13882 sincosq4sgn 13883 sinq12gt0 13884 abssinper 13900 coskpi 13902 rpcxpsqrt 13975 logsqrt 13976 |
Copyright terms: Public domain | W3C validator |