|   | 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 715 | . 2 ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜓) → 𝜒) | 
| 3 | 2 | adantlll 718 | 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: oaass 8600 oewordri 8631 naddssim 8724 infxp 10255 lediv12a 12162 xmulgt0 13326 ioodisj 13523 leexp1a 14216 swrdswrdlem 14743 seqshft 15125 sumss2 15763 prmdvdsncoprmbd 16765 mulgfval 19088 grpissubg 19165 f1otrspeq 19466 mat1dimcrng 22484 elcls 23082 neiptopreu 23142 alexsubALTlem4 24059 ustuqtop2 24252 iscfil2 25301 absmuls 28269 tglowdim1i 28510 axcontlem2 28981 opreu2reuALT 32497 nsgqusf1olem1 33442 lbslelsp 33649 matunitlindflem1 37624 matunitlindflem2 37625 poimirlem4 37632 founiiun0 45200 xralrple2 45370 rexabslelem 45434 climisp 45766 climxrre 45770 cnrefiisplem 45849 sge0iunmptlemre 46435 nnfoctbdjlem 46475 iundjiun 46480 meaiuninc3v 46504 hoidmvlelem3 46617 hspmbllem2 46647 smflimlem2 46792 | 
| Copyright terms: Public domain | W3C validator |