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 1363 | 1 ⊢ (𝜑 → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1079 |
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 208 df-an 397 df-3an 1081 |
This theorem is referenced by: rankcf 10187 bcpasc 13669 sqreulem 14707 qnumdencoprm 16073 qeqnumdivden 16074 xpsaddlem 16834 xpsvsca 16838 xpsle 16840 grpinvid 18098 qus0 18276 ghmid 18302 lsm01 18726 frgpadd 18818 abvneg 19534 lsmcv 19842 discmp 21934 kgenhaus 22080 idnghm 23279 xmetdcn2 23372 pi1addval 23579 ipcau2 23764 gausslemma2dlem1a 25868 2lgs 25910 uhgrsubgrself 26989 wlkl0 28073 carsgclctunlem2 31476 carsgclctun 31478 ballotlem1ri 31691 satefvfmla0 32562 satefvfmla1 32569 ftc1anclem5 34852 opoc1 36218 opoc0 36219 dochsat 38399 lcfrlem9 38566 relt0neg1 39122 pellfundex 39361 0ellimcdiv 41806 add2cncf 42062 stoweidlem21 42183 stoweidlem23 42185 stoweidlem32 42194 stoweidlem36 42198 stoweidlem40 42202 stoweidlem41 42203 mod42tp1mod8 43644 lincval0 44398 |
Copyright terms: Public domain | W3C validator |