Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ad4ant24 | 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 |
---|---|
ad4ant2.1 | ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
Ref | Expression |
---|---|
ad4ant24 | ⊢ ((((𝜃 ∧ 𝜑) ∧ 𝜏) ∧ 𝜓) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ad4ant2.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | |
2 | 1 | adantlr 711 | . 2 ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜓) → 𝜒) |
3 | 2 | adantlll 714 | 1 ⊢ ((((𝜃 ∧ 𝜑) ∧ 𝜏) ∧ 𝜓) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
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 |
This theorem is referenced by: oaass 8176 oewordri 8207 infxp 9625 lediv12a 11521 xmulgt0 12664 ioodisj 12856 leexp1a 13527 swrdswrdlem 14054 seqshft 14432 sumss2 15071 mulgfval 18164 grpissubg 18237 f1otrspeq 18504 mat1dimcrng 21014 elcls 21609 neiptopreu 21669 alexsubALTlem4 22586 ustuqtop2 22778 iscfil2 23796 tglowdim1i 26214 axcontlem2 26678 opreu2reuALT 30167 matunitlindflem1 34769 matunitlindflem2 34770 founiiun0 41327 xralrple2 41498 rexabslelem 41568 climisp 41903 climxrre 41907 cnrefiisplem 41986 sge0iunmptlemre 42574 nnfoctbdjlem 42614 iundjiun 42619 meaiuninc3v 42643 hoidmvlelem3 42756 hspmbllem2 42786 smflimlem2 42925 |
Copyright terms: Public domain | W3C validator |