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 1315 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜃) |
5 | 1, 4 | mpan2 422 | 1 ⊢ (𝜑 → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 967 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 969 |
This theorem is referenced by: sbciegf 2977 ac6sfi 6855 dju0en 7161 1qec 7320 ltaddnq 7339 halfnqq 7342 1idsr 7700 pn0sr 7703 ltm1sr 7709 muleqadd 8556 halfcl 9074 rehalfcl 9075 half0 9076 2halves 9077 halfpos2 9078 halfnneg2 9080 halfaddsub 9082 nneoor 9284 zeo 9287 fztp 10003 modqfrac 10262 iexpcyc 10549 bcn2 10666 bcpasc 10668 imre 10779 reim 10780 crim 10786 addcj 10819 imval2 10822 sinf 11631 efi4p 11644 resin4p 11645 recos4p 11646 sinneg 11653 efival 11659 cosadd 11664 sinmul 11671 sinbnd 11679 cosbnd 11680 ef01bndlem 11683 sin01bnd 11684 cos01bnd 11685 sin01gt0 11688 cos01gt0 11689 sin02gt0 11690 odd2np1lem 11794 odd2np1 11795 pythagtriplem12 12186 pockthi 12267 mopnex 13052 sincosq1lem 13293 sincosq2sgn 13295 sincosq3sgn 13296 sincosq4sgn 13297 sinq12gt0 13298 abssinper 13314 coskpi 13316 rpcxpsqrt 13389 logsqrt 13390 |
Copyright terms: Public domain | W3C validator |