Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3ad2antr3 | Structured version Visualization version GIF version |
Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 30-Dec-2007.) |
Ref | Expression |
---|---|
3ad2antl.1 | ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
3ad2antr3 | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3ad2antl.1 | . . 3 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) | |
2 | 1 | adantrl 712 | . 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜒)) → 𝜃) |
3 | 2 | 3adantr1 1161 | 1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1079 |
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 208 df-an 397 df-3an 1081 |
This theorem is referenced by: simpr3 1188 simpr3l 1226 simpr3r 1227 simpr31 1255 simpr32 1256 simpr33 1257 fpr2g 6965 frfi 8751 ressress 16550 funcestrcsetclem9 17386 funcsetcestrclem9 17401 latjjdir 17702 grprcan 18075 grpsubrcan 18118 grpaddsubass 18127 mhmmnd 18159 zntoslem 20631 ipdir 20711 ipass 20717 qustgpopn 22655 extwwlkfab 28058 grpomuldivass 28245 nvmdi 28352 dmdsl3 30019 dvrcan5 30791 imaslmod 30849 esum2d 31251 voliune 31387 btwnconn1lem7 33451 poimirlem4 34777 cvrnbtwn4 36295 paddasslem14 36849 paddasslem17 36852 paddss 36861 pmod1i 36864 cdleme1 37243 cdleme2 37244 xlimbr 41984 sbgoldbst 43820 funcringcsetcALTV2lem9 44243 funcringcsetclem9ALTV 44266 |
Copyright terms: Public domain | W3C validator |