| 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 1129 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) |
| 5 | mp3and.4 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)) | |
| 6 | 4, 5 | mpd 15 | 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: eqsupd 9497 eqinfd 9525 updjud 9974 fvf1tp 13829 mreexexlemd 17687 mhmlem 19080 nn0gsumfz 20002 mdetunilem3 22620 mdetunilem9 22626 axtgupdim2 28479 axtgeucl 28480 wwlksnextprop 29932 measdivcst 34225 btwnouttr2 36023 btwnexch2 36024 cgrsub 36046 btwnconn1lem2 36089 btwnconn1lem5 36092 btwnconn1lem6 36093 segcon2 36106 btwnoutside 36126 broutsideof3 36127 outsideoftr 36130 outsideofeq 36131 lineelsb2 36149 relowlssretop 37364 lshpkrlem6 39116 reladdrsub 42415 onsupuni 43241 omabs2 43345 modelaxreplem2 44996 fmuldfeq 45598 stoweidlem5 46020 el0ldep 48383 ldepspr 48390 |
| Copyright terms: Public domain | W3C validator |