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 1321 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜃) |
5 | 1, 4 | mpan2 423 | 1 ⊢ (𝜑 → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 973 |
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 975 |
This theorem is referenced by: sbciegf 2986 ac6sfi 6876 dju0en 7191 1qec 7350 ltaddnq 7369 halfnqq 7372 1idsr 7730 pn0sr 7733 ltm1sr 7739 muleqadd 8586 halfcl 9104 rehalfcl 9105 half0 9106 2halves 9107 halfpos2 9108 halfnneg2 9110 halfaddsub 9112 nneoor 9314 zeo 9317 fztp 10034 modqfrac 10293 iexpcyc 10580 bcn2 10698 bcpasc 10700 imre 10815 reim 10816 crim 10822 addcj 10855 imval2 10858 sinf 11667 efi4p 11680 resin4p 11681 recos4p 11682 sinneg 11689 efival 11695 cosadd 11700 sinmul 11707 sinbnd 11715 cosbnd 11716 ef01bndlem 11719 sin01bnd 11720 cos01bnd 11721 sin01gt0 11724 cos01gt0 11725 sin02gt0 11726 odd2np1lem 11831 odd2np1 11832 pythagtriplem12 12229 pockthi 12310 mopnex 13299 sincosq1lem 13540 sincosq2sgn 13542 sincosq3sgn 13543 sincosq4sgn 13544 sinq12gt0 13545 abssinper 13561 coskpi 13563 rpcxpsqrt 13636 logsqrt 13637 |
Copyright terms: Public domain | W3C validator |