| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > ad5ant14 | Structured version Visualization version GIF version | ||
| Description: Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.) |
| Ref | Expression |
|---|---|
| ad5ant2.1 | ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
| Ref | Expression |
|---|---|
| ad5ant14 | ⊢ (((((𝜑 ∧ 𝜃) ∧ 𝜏) ∧ 𝜓) ∧ 𝜂) → 𝜒) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ad5ant2.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | |
| 2 | 1 | adantlr 715 | . 2 ⊢ (((𝜑 ∧ 𝜃) ∧ 𝜓) → 𝜒) |
| 3 | 2 | ad4ant13 751 | 1 ⊢ (((((𝜑 ∧ 𝜃) ∧ 𝜏) ∧ 𝜓) ∧ 𝜂) → 𝜒) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 |
| 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 |
| This theorem is referenced by: leexp1a 14215 cpmatinvcl 22723 restcld 23180 ustuqtop3 24252 legval 28592 ccatws1f1o 32936 lssdimle 33658 zarcls1 33868 lindsenlbs 37622 matunitlindflem1 37623 modelaxrep 44998 xrralrecnnle 45394 limclner 45666 limsupub2 45827 xlimliminflimsup 45877 pimdecfgtioo 46732 pimincfltioo 46733 |
| Copyright terms: Public domain | W3C validator |