![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3adant3r1 | Structured version Visualization version GIF version |
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Feb-2008.) |
Ref | Expression |
---|---|
ad4ant3.1 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
3adant3r1 | ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓 ∧ 𝜒)) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ad4ant3.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
2 | 1 | 3expb 1121 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
3 | 2 | 3adantr1 1170 | 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: dif1en 9156 ccatswrd 14614 plttr 18291 pltletr 18292 latjlej1 18402 latjlej2 18403 latnlej 18405 latnlej2 18408 latmlem2 18419 latledi 18426 latjass 18432 latj32 18434 latj13 18435 ipopos 18485 tsrlemax 18535 imasmnd2 18658 grpsubsub 18908 grpnnncan2 18916 imasgrp2 18934 mulgnn0ass 18984 mulgsubdir 18988 cmn32 19661 ablsubadd 19669 imasring 20133 zntoslem 21096 xmettri3 23841 mettri3 23842 xmetrtri 23843 xmetrtri2 23844 metrtri 23845 cphdivcl 24681 cphassr 24711 relogbmulexp 26263 grpodivdiv 29771 grpomuldivass 29772 ablo32 29780 ablodivdiv4 29785 ablodiv32 29786 nvmdi 29879 dipdi 30074 dipassr 30077 dipsubdir 30079 dipsubdi 30080 dvrcan5 32360 cgr3tr4 34962 cgr3rflx 34964 endofsegid 34995 seglemin 35023 broutsideof2 35032 rngosubdi 36751 rngosubdir 36752 isdrngo2 36764 crngm23 36808 dmncan2 36883 latmassOLD 38037 latm32 38039 cvrnbtwn4 38087 cvrcmp2 38092 ltcvrntr 38233 atcvrj0 38237 3dim3 38278 paddasslem17 38645 paddass 38647 lautlt 38900 lautcvr 38901 lautj 38902 lautm 38903 erngdvlem3 39799 dvalveclem 39834 isdomn4 40970 mendlmod 41868 imasrng 46613 |
Copyright terms: Public domain | W3C validator |