| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > 3adant3r | Structured version Visualization version GIF version | ||
| Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 25-Jun-2022.) |
| Ref | Expression |
|---|---|
| ad4ant3.1 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
| Ref | Expression |
|---|---|
| 3adant3r | ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜏)) → 𝜃) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | simpl 482 | . 2 ⊢ ((𝜒 ∧ 𝜏) → 𝜒) | |
| 2 | ad4ant3.1 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
| 3 | 1, 2 | syl3an3 1166 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜏)) → 𝜃) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∧ 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: wfrlem12OLD 8360 mapfien2 9449 cfeq0 10296 ltmul2 12118 lemul1 12119 lemul2 12120 lemuldiv 12148 lediv2 12158 ltdiv23 12159 lediv23 12160 dvdscmulr 16322 dvdsmulcr 16323 modremain 16445 ndvdsadd 16447 rpexp12i 16761 isdrngd 20765 isdrngdOLD 20767 cramerimp 22692 tsmsxp 24163 xblcntrps 24420 xblcntr 24421 rrxmet 25442 nvaddsub4 30676 hvmulcan2 31092 adjlnop 32105 rrnmet 37836 lfladd 39067 lflsub 39068 lshpset2N 39120 atcvrj1 39433 athgt 39458 ltrncnvel 40144 trlcnv 40167 trljat2 40169 cdlemc5 40197 trlcoabs 40723 trlcolem 40728 dicvaddcl 41192 limsupre3uzlem 45750 fourierdlem42 46164 ovnhoilem2 46617 lincext3 48373 |
| Copyright terms: Public domain | W3C validator |