![]() |
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 1337 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜃) |
5 | 1, 4 | mpan2 425 | 1 ⊢ (𝜑 → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 980 |
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 982 |
This theorem is referenced by: sbciegf 3009 ac6sfi 6927 dju0en 7244 1qec 7418 ltaddnq 7437 halfnqq 7440 1idsr 7798 pn0sr 7801 ltm1sr 7807 muleqadd 8656 halfcl 9176 rehalfcl 9177 half0 9178 2halves 9179 halfpos2 9180 halfnneg2 9182 halfaddsub 9184 nneoor 9386 zeo 9389 fztp 10110 modqfrac 10370 iexpcyc 10659 bcn2 10779 bcpasc 10781 imre 10895 reim 10896 crim 10902 addcj 10935 imval2 10938 sinf 11747 efi4p 11760 resin4p 11761 recos4p 11762 sinneg 11769 efival 11775 cosadd 11780 sinmul 11787 sinbnd 11795 cosbnd 11796 ef01bndlem 11799 sin01bnd 11800 cos01bnd 11801 sin01gt0 11804 cos01gt0 11805 sin02gt0 11806 odd2np1lem 11912 odd2np1 11913 pythagtriplem12 12310 pockthi 12393 opprsubrngg 13575 isridl 13836 zlmval 13940 zlmlemg 13941 zlmsca 13945 zlmvscag 13946 mopnex 14482 sincosq1lem 14723 sincosq2sgn 14725 sincosq3sgn 14726 sincosq4sgn 14727 sinq12gt0 14728 abssinper 14744 coskpi 14746 rpcxpsqrt 14819 logsqrt 14820 2lgsoddprmlem2 14932 |
Copyright terms: Public domain | W3C validator |