![]() |
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 754 | . 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜒)) → 𝜃) |
3 | 2 | 3adantr1 1175 | 1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1072 |
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 197 df-an 385 df-3an 1074 |
This theorem is referenced by: simpr3 1238 simpr3l 1299 simpr3r 1301 simpr31 1345 simpr32 1347 simpr33 1349 fpr2g 6640 frfi 8372 ressress 16160 funcestrcsetclem9 17009 funcsetcestrclem9 17024 latjjdir 17325 grprcan 17676 grpsubrcan 17717 grpaddsubass 17726 mhmmnd 17758 zntoslem 20127 ipdir 20206 ipass 20212 qustgpopn 22144 extwwlkfab 27532 grpomuldivass 27725 nvmdi 27833 dmdsl3 29504 dvrcan5 30123 esum2d 30485 voliune 30622 btwnconn1lem7 32527 poimirlem4 33744 cvrnbtwn4 35087 paddasslem14 35640 paddasslem17 35643 paddss 35652 pmod1i 35655 cdleme1 36035 cdleme2 36036 xlimbr 40574 sbgoldbst 42194 funcringcsetcALTV2lem9 42572 funcringcsetclem9ALTV 42595 |
Copyright terms: Public domain | W3C validator |