![]() |
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 1108 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) |
5 | mp3and.4 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)) | |
6 | 4, 5 | mpd 15 | 1 ⊢ (𝜑 → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1068 |
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 199 df-an 388 df-3an 1070 |
This theorem is referenced by: eqsupd 8716 eqinfd 8744 updjud 9157 mreexexlemd 16773 mhmlem 18006 nn0gsumfz 18854 mdetunilem3 20927 mdetunilem9 20933 axtgupdim2 25959 axtgeucl 25960 wwlksnextprop 27415 wwlksnextpropOLD 27416 measdivcst 31126 noprefixmo 32720 btwnouttr2 33001 btwnexch2 33002 cgrsub 33024 btwnconn1lem2 33067 btwnconn1lem5 33070 btwnconn1lem6 33071 segcon2 33084 btwnoutside 33104 broutsideof3 33105 outsideoftr 33108 outsideofeq 33109 lineelsb2 33127 relowlssretop 34083 lshpkrlem6 35693 reladdrsub 38645 fmuldfeq 41293 stoweidlem5 41719 el0ldep 43886 ldepspr 43893 |
Copyright terms: Public domain | W3C validator |