![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mp3and | Structured version Visualization version GIF version |
Description: A deduction based on modus ponens. (Contributed by Mario Carneiro, 24-Dec-2016.) |
Ref | Expression |
---|---|
mp3and.1 | ⊢ (𝜑 → 𝜓) |
mp3and.2 | ⊢ (𝜑 → 𝜒) |
mp3and.3 | ⊢ (𝜑 → 𝜃) |
mp3and.4 | ⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)) |
Ref | Expression |
---|---|
mp3and | ⊢ (𝜑 → 𝜏) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mp3and.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | mp3and.2 | . . 3 ⊢ (𝜑 → 𝜒) | |
3 | mp3and.3 | . . 3 ⊢ (𝜑 → 𝜃) | |
4 | 1, 2, 3 | 3jca 1125 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) |
5 | mp3and.4 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)) | |
6 | 4, 5 | mpd 15 | 1 ⊢ (𝜑 → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1084 |
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 395 df-3an 1086 |
This theorem is referenced by: eqsupd 9493 eqinfd 9521 updjud 9970 mreexexlemd 17652 mhmlem 19052 nn0gsumfz 19978 mdetunilem3 22604 mdetunilem9 22610 axtgupdim2 28395 axtgeucl 28396 wwlksnextprop 29843 measdivcst 34070 btwnouttr2 35859 btwnexch2 35860 cgrsub 35882 btwnconn1lem2 35925 btwnconn1lem5 35928 btwnconn1lem6 35929 segcon2 35942 btwnoutside 35962 broutsideof3 35963 outsideoftr 35966 outsideofeq 35967 lineelsb2 35985 relowlssretop 37083 lshpkrlem6 38826 reladdrsub 42096 onsupuni 42931 omabs2 43035 fmuldfeq 45240 stoweidlem5 45662 el0ldep 47885 ldepspr 47892 |
Copyright terms: Public domain | W3C validator |