| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > 3ad2antr2 | Structured version Visualization version GIF version | ||
| Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 27-Dec-2007.) |
| Ref | Expression |
|---|---|
| 3ad2antl.1 | ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
| Ref | Expression |
|---|---|
| 3ad2antr2 | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 3ad2antl.1 | . . 3 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) | |
| 2 | 1 | adantrl 716 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
| 3 | 2 | 3adantr3 1172 | 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: simpr2 1196 simpr2l 1233 simpr2r 1234 simpr21 1261 simpr22 1262 simpr23 1263 wereu 5681 axdc4lem 10495 ioc0 13434 funcestrcsetclem9 18193 funcsetcestrclem9 18208 grpsubadd 19046 zntoslem 21575 mdsl3 32335 dvrcan5 33240 idlsrgmnd 33542 prv1n 35436 brofs2 36078 brifs2 36079 poimirlem28 37655 ftc1anc 37708 frinfm 37742 welb 37743 fdc 37752 unichnidl 38038 cvrnbtwn2 39276 islpln2a 39550 paddss1 39819 paddss2 39820 paddasslem17 39838 tendospass 41021 funcringcsetcALTV2lem9 48214 funcringcsetclem9ALTV 48237 ldepsprlem 48389 |
| Copyright terms: Public domain | W3C validator |