| 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 714 | . 2 ⊢ (((𝜏 ∧ 𝜑) ∧ 𝜒) → 𝜃) |
| 3 | 2 | 3adantl1 1167 | 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: simpl3 1194 simpl3l 1229 simpl3r 1230 simpl31 1255 simpl32 1256 simpl33 1257 rspc3ev 3639 brcogw 5879 cocan1 7311 ov6g 7597 fpr1 8328 dif1enlem 9196 dif1ennnALT 9311 cfsmolem 10310 coftr 10313 axcc3 10478 axdc4lem 10495 gruf 10851 dedekindle 11425 zdivmul 12690 cshf1 14848 cshimadifsn 14868 fprodle 16032 bpolycl 16088 lcmdvds 16645 lubss 18558 odeq 19568 ghmplusg 19864 lmhmvsca 21044 islindf4 21858 mndifsplit 22642 gsummatr01lem3 22663 gsummatr01 22665 mp2pm2mplem4 22815 elcls 23081 cnpresti 23296 cmpsublem 23407 comppfsc 23540 ptpjcn 23619 elfm3 23958 rnelfmlem 23960 nmoix 24750 caublcls 25343 ig1pdvds 26219 coeid3 26279 amgm 27034 brbtwn2 28920 colinearalg 28925 axsegconlem1 28932 ax5seglem1 28943 ax5seglem2 28944 homco1 31820 hoadddi 31822 br6 35757 lindsenlbs 37622 upixp 37736 filbcmb 37747 3dim1 39469 llni 39510 lplni 39534 lvoli 39577 cdleme42mgN 40490 mzprename 42760 infmrgelbi 42889 relexpxpmin 43730 n0p 45050 rexabslelem 45429 pimxrneun 45499 limcleqr 45659 fnlimfvre 45689 stoweidlem17 46032 stoweidlem28 46043 fourierdlem12 46134 fourierdlem41 46163 fourierdlem42 46164 fourierdlem74 46195 fourierdlem77 46198 qndenserrnopnlem 46312 issalnnd 46360 hspmbllem2 46642 issmfle 46760 smflimlem2 46787 smflimmpt 46825 smfinflem 46832 smflimsuplem7 46841 smflimsupmpt 46844 smfliminfmpt 46847 lighneallem3 47594 |
| Copyright terms: Public domain | W3C validator |