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 483 | . 2 ⊢ ((𝜒 ∧ 𝜏) → 𝜒) | |
2 | ad4ant3.1 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
3 | 1, 2 | syl3an3 1157 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜏)) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1079 |
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 df-3an 1081 |
This theorem is referenced by: wfrlem12 7955 mapfien2 8860 cfeq0 9666 ltmul2 11479 lemul1 11480 lemul2 11481 lemuldiv 11508 lediv2 11518 ltdiv23 11519 lediv23 11520 dvdscmulr 15626 dvdsmulcr 15627 modremain 15747 ndvdsadd 15749 rpexp12i 16054 isdrngd 19456 cramerimp 21223 tsmsxp 22690 xblcntrps 22947 xblcntr 22948 rrxmet 23938 nvaddsub4 28361 hvmulcan2 28777 adjlnop 29790 rrnmet 34988 lfladd 36082 lflsub 36083 lshpset2N 36135 atcvrj1 36447 athgt 36472 ltrncnvel 37158 trlcnv 37181 trljat2 37183 cdlemc5 37211 trlcoabs 37737 trlcolem 37742 dicvaddcl 38206 limsupre3uzlem 41892 fourierdlem42 42311 ovnhoilem2 42761 lincext3 44439 |
Copyright terms: Public domain | W3C validator |