![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3adant3r | Structured version Visualization version GIF version |
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 25-Jun-2022.) |
Ref | Expression |
---|---|
ad4ant3.1 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
3adant3r | ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜏)) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl 484 | . 2 ⊢ ((𝜒 ∧ 𝜏) → 𝜒) | |
2 | ad4ant3.1 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
3 | 1, 2 | syl3an3 1166 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜏)) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∧ w3a 1088 |
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 206 df-an 398 df-3an 1090 |
This theorem is referenced by: wfrlem12OLD 8267 mapfien2 9346 cfeq0 10193 ltmul2 12007 lemul1 12008 lemul2 12009 lemuldiv 12036 lediv2 12046 ltdiv23 12047 lediv23 12048 dvdscmulr 16168 dvdsmulcr 16169 modremain 16291 ndvdsadd 16293 rpexp12i 16601 isdrngd 20215 isdrngdOLD 20217 cramerimp 22038 tsmsxp 23509 xblcntrps 23766 xblcntr 23767 rrxmet 24775 nvaddsub4 29602 hvmulcan2 30018 adjlnop 31031 rrnmet 36291 lfladd 37531 lflsub 37532 lshpset2N 37584 atcvrj1 37897 athgt 37922 ltrncnvel 38608 trlcnv 38631 trljat2 38633 cdlemc5 38661 trlcoabs 39187 trlcolem 39192 dicvaddcl 39656 limsupre3uzlem 43983 fourierdlem42 44397 ovnhoilem2 44850 lincext3 46544 |
Copyright terms: Public domain | W3C validator |