![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3ad2antl3 | Structured version Visualization version GIF version |
Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.) |
Ref | Expression |
---|---|
3ad2antl.1 | ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
3ad2antl3 | ⊢ (((𝜓 ∧ 𝜏 ∧ 𝜑) ∧ 𝜒) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3ad2antl.1 | . . 3 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) | |
2 | 1 | adantll 702 | . 2 ⊢ (((𝜏 ∧ 𝜑) ∧ 𝜒) → 𝜃) |
3 | 2 | 3adantl1 1147 | 1 ⊢ (((𝜓 ∧ 𝜏 ∧ 𝜑) ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 ∧ w3a 1069 |
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 1071 |
This theorem is referenced by: simpl3 1174 simpl3l 1209 simpl3r 1210 simpl31 1235 simpl32 1236 simpl33 1237 rspc3ev 3545 brcogw 5585 cocan1 6870 ov6g 7126 dif1en 8544 cfsmolem 9488 coftr 9491 axcc3 9656 axdc4lem 9673 gruf 10029 dedekindle 10602 zdivmul 11865 cshf1 14032 cshimadifsn 14051 fprodle 15208 bpolycl 15264 lcmdvds 15806 lubss 17601 gsumccat 17858 odeq 18452 ghmplusg 18734 lmhmvsca 19551 islindf4 20699 mndifsplit 20964 gsummatr01lem3 20985 gsummatr01 20987 mp2pm2mplem4 21136 elcls 21400 cnpresti 21615 cmpsublem 21726 comppfsc 21859 ptpjcn 21938 elfm3 22277 rnelfmlem 22279 nmoix 23056 caublcls 23630 ig1pdvds 24488 coeid3 24548 amgm 25285 brbtwn2 26409 colinearalg 26414 axsegconlem1 26421 ax5seglem1 26432 ax5seglem2 26433 homco1 29374 hoadddi 29376 br6 32550 fpr1 32697 lindsenlbs 34365 upixp 34483 filbcmb 34494 3dim1 36085 llni 36126 lplni 36150 lvoli 36193 cdleme42mgN 37106 mzprename 38779 infmrgelbi 38909 relexpxpmin 39463 n0p 40762 rexabslelem 41157 limcleqr 41390 fnlimfvre 41420 stoweidlem17 41767 stoweidlem28 41778 fourierdlem12 41869 fourierdlem41 41898 fourierdlem42 41899 fourierdlem74 41930 fourierdlem77 41933 qndenserrnopnlem 42047 issalnnd 42093 hspmbllem2 42374 issmfle 42487 smflimlem2 42513 smflimmpt 42549 smfinflem 42556 smflimsuplem7 42565 smflimsupmpt 42568 smfliminfmpt 42571 lighneallem3 43174 |
Copyright terms: Public domain | W3C validator |