| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > mpd3an23 | Structured version Visualization version GIF version | ||
| Description: An inference based on modus ponens. (Contributed by NM, 4-Dec-2006.) |
| Ref | Expression |
|---|---|
| mpd3an23.1 | ⊢ (𝜑 → 𝜓) |
| mpd3an23.2 | ⊢ (𝜑 → 𝜒) |
| mpd3an23.3 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
| Ref | Expression |
|---|---|
| mpd3an23 | ⊢ (𝜑 → 𝜃) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | id 22 | . 2 ⊢ (𝜑 → 𝜑) | |
| 2 | mpd3an23.1 | . 2 ⊢ (𝜑 → 𝜓) | |
| 3 | mpd3an23.2 | . 2 ⊢ (𝜑 → 𝜒) | |
| 4 | mpd3an23.3 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
| 5 | 1, 2, 3, 4 | syl3anc 1373 | 1 ⊢ (𝜑 → 𝜃) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ w3a 1087 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-3an 1089 |
| This theorem is referenced by: rankcf 10817 bcpasc 14360 sqreulem 15398 qnumdencoprm 16782 qeqnumdivden 16783 xpsaddlem 17618 xpsvsca 17622 xpsle 17624 grpinvid 19017 qus0 19207 ghmid 19240 lsm01 19689 frgpadd 19781 abvneg 20827 lsmcv 21143 qusmul2idl 21289 discmp 23406 kgenhaus 23552 idnghm 24764 xmetdcn2 24859 pi1addval 25081 ipcau2 25268 gausslemma2dlem1a 27409 2lgs 27451 etasslt2 27859 uhgrsubgrself 29297 wlkl0 30386 mhmimasplusg 33043 lmhmimasvsca 33044 rlocaddval 33272 rlocmulval 33273 qusvsval 33380 carsgclctunlem2 34321 carsgclctun 34323 ballotlem1ri 34537 satefvfmla0 35423 satefvfmla1 35430 ftc1anclem5 37704 opoc1 39203 opoc0 39204 dochsat 41385 lcfrlem9 41552 fisdomnn 42285 pellfundex 42897 mnringmulrcld 44247 0ellimcdiv 45664 add2cncf 45917 stoweidlem21 46036 stoweidlem23 46038 stoweidlem32 46047 stoweidlem36 46051 stoweidlem40 46055 stoweidlem41 46056 natglobalincr 46892 mod42tp1mod8 47589 lincval0 48332 |
| Copyright terms: Public domain | W3C validator |