![]() |
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 1122 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) |
5 | mp3and.4 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)) | |
6 | 4, 5 | mpd 15 | 1 ⊢ (𝜑 → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1071 |
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 197 df-an 383 df-3an 1073 |
This theorem is referenced by: eqsupd 8523 eqinfd 8551 updjud 8964 mreexexlemd 16512 mhmlem 17743 nn0gsumfz 18587 mdetunilem3 20638 mdetunilem9 20644 axtgeucl 25592 wwlksnextprop 27057 measdivcst 30628 noprefixmo 32185 btwnouttr2 32466 btwnexch2 32467 cgrsub 32489 btwnconn1lem2 32532 btwnconn1lem5 32535 btwnconn1lem6 32536 segcon2 32549 btwnoutside 32569 broutsideof3 32570 outsideoftr 32573 outsideofeq 32574 lineelsb2 32592 relowlssretop 33547 lshpkrlem6 34922 fmuldfeq 40328 stoweidlem5 40734 el0ldep 42778 ldepspr 42785 |
Copyright terms: Public domain | W3C validator |