|   | 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 716 | . 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜒)) → 𝜃) | 
| 3 | 2 | 3adantr1 1170 | 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: simpr3 1197 simpr3l 1235 simpr3r 1236 simpr31 1264 simpr32 1265 simpr33 1266 fpr2g 7231 frfi 9321 ressress 17293 funcestrcsetclem9 18193 funcsetcestrclem9 18208 latjjdir 18537 grprcan 18991 grpsubrcan 19039 grpaddsubass 19048 mhmmnd 19082 zntoslem 21575 ipdir 21657 ipass 21663 qustgpopn 24128 extwwlkfab 30371 grpomuldivass 30560 nvmdi 30667 dmdsl3 32334 dvrcan5 33240 imaslmod 33381 idlsrgmnd 33542 esum2d 34094 voliune 34230 btwnconn1lem7 36094 poimirlem4 37631 cvrnbtwn4 39280 paddasslem14 39835 paddasslem17 39838 paddss 39847 pmod1i 39850 cdleme1 40229 cdleme2 40230 xlimbr 45842 sbgoldbst 47765 funcringcsetcALTV2lem9 48214 funcringcsetclem9ALTV 48237 | 
| Copyright terms: Public domain | W3C validator |