![]() |
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 1372 | 1 ⊢ (𝜑 → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1088 |
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 206 df-an 398 df-3an 1090 |
This theorem is referenced by: rankcf 10767 bcpasc 14276 sqreulem 15301 qnumdencoprm 16676 qeqnumdivden 16677 xpsaddlem 17514 xpsvsca 17518 xpsle 17520 grpinvid 18879 qus0 19061 ghmid 19091 lsm01 19531 frgpadd 19623 abvneg 20429 lsmcv 20741 qusmul2 20861 discmp 22883 kgenhaus 23029 idnghm 24241 xmetdcn2 24334 pi1addval 24545 ipcau2 24732 gausslemma2dlem1a 26847 2lgs 26889 etasslt2 27294 uhgrsubgrself 28516 wlkl0 29599 qusvsval 32435 qusmul 32479 carsgclctunlem2 33255 carsgclctun 33257 ballotlem1ri 33470 satefvfmla0 34346 satefvfmla1 34353 ftc1anclem5 36502 opoc1 38009 opoc0 38010 dochsat 40191 lcfrlem9 40358 pellfundex 41556 mnringmulrcld 42919 0ellimcdiv 44299 add2cncf 44552 stoweidlem21 44671 stoweidlem23 44673 stoweidlem32 44682 stoweidlem36 44686 stoweidlem40 44690 stoweidlem41 44691 natglobalincr 45525 mod42tp1mod8 46204 lincval0 46997 |
Copyright terms: Public domain | W3C validator |