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 1318 | 1 ⊢ (𝜑 → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1031 |
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 196 df-an 385 df-3an 1033 |
This theorem is referenced by: rankcf 9478 bcpasc 12970 sqreulem 13947 qnumdencoprm 15291 qeqnumdivden 15292 xpsaddlem 16058 xpsvsca 16062 xpsle 16064 grpinvid 17299 qus0 17475 ghmid 17489 lsm01 17907 frgpadd 17999 abvneg 18657 lsmcv 18962 discmp 21011 kgenhaus 21157 idnghm 22357 xmetdcn2 22448 pi1addval 22656 ipcau2 22841 gausslemma2dlem1a 24890 2lgs 24932 carsgclctunlem2 29708 carsgclctun 29710 ballotlem1ri 29923 ftc1anclem5 32659 opoc1 33507 opoc0 33508 dochsat 35690 lcfrlem9 35857 pellfundex 36468 0ellimcdiv 38716 add2cncf 38789 stoweidlem21 38914 stoweidlem23 38916 stoweidlem32 38925 stoweidlem36 38929 stoweidlem40 38933 stoweidlem41 38934 mod42tp1mod8 40057 uhgrsubgrself 40504 lincval0 41998 |
Copyright terms: Public domain | W3C validator |